X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=1caeb733db2a21253b996e91893f77df8a0d4878;hb=a3c9916401dbaac8e59948e878eec0f37e72bf4a;hp=f01ecf785ed8524f5002d6c3f6e08610a617bdbb;hpb=f17da39739c49297bf435896c8cb4e3ac83b95a6;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f01ecf785..1caeb733d 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1013,22 +1013,22 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
   and eat_prods 
     allow_coercions subst metasenv context hetype tlbody_and_type ugraph 
   =
-    let rec mk_prod metasenv context =
+    let rec mk_prod metasenv context' =
       function
           [] ->
             let (metasenv, idx) = 
-              CicMkImplicit.mk_implicit_type metasenv subst context 
+              CicMkImplicit.mk_implicit_type metasenv subst context'
             in
             let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context
+              CicMkImplicit.identity_relocation_list_for_metavariable context'
             in
               metasenv,Cic.Meta (idx, irl)
         | (_,argty)::tl ->
             let (metasenv, idx) = 
-              CicMkImplicit.mk_implicit_type metasenv subst context 
+              CicMkImplicit.mk_implicit_type metasenv subst context' 
             in
             let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context
+              CicMkImplicit.identity_relocation_list_for_metavariable context'
             in
             let meta = Cic.Meta (idx,irl) in
             let name =
@@ -1036,7 +1036,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               (* Nevertheless, argty is well-typed only in context.  *)
               (* Thus I generate a name (name_hint) in context and   *)
               (* then I generate a name --- using the hint name_hint *)
-              (* --- that is fresh in (context'@context).            *)
+              (* --- that is fresh in context'.                      *)
               let name_hint = 
                 (* Cic.Name "pippo" *)
                 FreshNamesGenerator.mk_fresh_name ~subst metasenv 
@@ -1047,10 +1047,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               in
                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
                 FreshNamesGenerator.mk_fresh_name ~subst
-                  [] context name_hint ~typ:(Cic.Sort Cic.Prop)
+                  [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
             in
             let metasenv,target =
-              mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+              mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
             in
               metasenv,Cic.Prod (name,meta,target)
     in