restored the right context used to generate names. see the comment

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index e4f4ef8e0c002a600f791d37ec2f9524730dbefb..49c85a72eea1b0fc09efb2d805f988040f12d4e4 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -166,7 +166,7 @@ let more_args_than_expected localization_tbl metasenv subst he context hetype' r
   enrich localization_tbl he ~f:(fun _-> msg) exn
 ;; 
 
-let mk_prod_of_metas metasenv context' subst args = 
+let mk_prod_of_metas metasenv context subst args = 
   let rec mk_prod metasenv context' = function
     | [] ->
         let (metasenv, idx) = 
@@ -191,14 +191,11 @@ let mk_prod_of_metas metasenv context' subst args =
           (* then I generate a name --- using the hint name_hint *)
           (* --- that is fresh in context'.                      *)
           let name_hint = 
-            (* Cic.Name "pippo" *)
             FreshNamesGenerator.mk_fresh_name ~subst metasenv 
-              (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
-              (CicMetaSubst.apply_subst_context subst context')
+              (CicMetaSubst.apply_subst_context subst context)
               Cic.Anonymous
               ~typ:(CicMetaSubst.apply_subst subst argty) 
           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)
         in
@@ -207,7 +204,7 @@ let mk_prod_of_metas metasenv context' subst args =
         in
           metasenv,Cic.Prod (name,meta,target)
   in
-  mk_prod metasenv context' args
+  mk_prod metasenv context args
 ;;
   
 let rec type_of_constant uri ugraph =