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

[helm.git] / components / cic_unification / cicRefine.ml

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e0f8fd1c79128ad1663640690a167c931ce623cb..49c85a72eea1b0fc09efb2d805f988040f12d4e4 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -91,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
   try
    Cic.CicHash.find localization_tbl t
   with Not_found ->
-   prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
+   HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
    raise exn'
  in
   raise (HExtlib.Localized (loc,exn'))
@@ -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 =
@@ -1334,7 +1331,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
                 " <==> " ^
-                CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+                CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
+                "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+                context));
                 debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
                 let subst,metasenv,ugraph =