X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=d52b8aa7c66b77d041c1ba5b151e9e9606b84044;hb=d5e51ef07afd46594ba980154f5f111afda7fcd9;hp=e4f4ef8e0c002a600f791d37ec2f9524730dbefb;hpb=dc151c78b57bae7de8ec8417925ade6c0d7b1db0;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index e4f4ef8e0..d52b8aa7c 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 =
@@ -571,7 +568,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              exn ->
               enrich localization_tbl term' exn
                ~f:(function _ ->
-                 lazy ("(10)The term " ^
+                 lazy ("The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
@@ -616,7 +613,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     exn ->
                      enrich localization_tbl constructor'
                       ~f:(fun _ ->
-                        lazy ("(11)The term " ^
+                        lazy ("The term " ^
                          CicMetaSubst.ppterm_in_context metasenv subst p'
                           context ^ " has type " ^
                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
@@ -803,7 +800,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       exn ->
                        enrich localization_tbl p exn
                         ~f:(function _ ->
-                          lazy ("(12)The term " ^
+                          lazy ("The term " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
@@ -844,7 +841,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("(13)The term " ^
+                         lazy ("The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -897,7 +894,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("(14)The term " ^
+                         lazy ("The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1376,10 +1373,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
           fo_unif_subst subst context metasenv infty expty ugraph
         in
         (t, expty), subst, metasenv, ugraph
-      with Uncertain _ | RefineFailure _ as exn ->
-        if not allow_coercions || not !insert_coercions then
-          enrich localization_tbl t exn
-        else
+      with (Uncertain _ | RefineFailure _ as exn)
+        when allow_coercions && !insert_coercions ->
           let whd = CicReduction.whd ~delta:false in
           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
           let infty = clean infty subst context in