From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 23 Nov 2007 17:59:19 +0000 (+0000)
Subject: restored the right context used to generate names. see the comment
X-Git-Tag: make_still_working~5787
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4a2768c670a6904975fe6098c5bf7ea80ddb49e8;p=helm.git

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 e4f4ef8e0..49c85a72e 100644
--- 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 =