More refinement errors localized.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 3faee32df31fbd8c48e2976a6cd5ccc9f02aba04..b9c5b0c6a642e50210edf3a579e1824da510d8c2 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -522,7 +522,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
               eat_prods true subst'' metasenv'' context 
-                hetype tlbody_and_type ugraph2
+                he hetype tlbody_and_type ugraph2
             in
               avoid_double_coercion context 
                 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
@@ -812,7 +812,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              in
              let _,_,subst,metasenv,ugraph4 =
                eat_prods false subst metasenv context 
-                 outtypety tlbody_and_type ugraph4
+                 outtype outtypety tlbody_and_type ugraph4
              in
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
@@ -1095,8 +1095,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             let (metasenv,idx) =
               CicMkImplicit.mk_implicit_sort metasenv subst in
             let (subst, metasenv,ugraph1) =
+             try
               fo_unif_subst subst context_for_t2 metasenv 
                 (C.Meta (idx,[])) t2'' ugraph
+             with _ -> assert false (* unification against a metavariable *)
             in
               t2'',subst,metasenv,ugraph1
         | _,_ -> 
@@ -1110,7 +1112,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (CicPp.ppterm t2''))))
 
   and eat_prods 
-    allow_coercions subst metasenv context hetype tlbody_and_type ugraph 
+    allow_coercions subst metasenv context he hetype tlbody_and_type ugraph 
   =
     let rec mk_prod metasenv context' =
       function
@@ -1158,14 +1160,16 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       try
         fo_unif_subst subst context metasenv hetype hetype' ugraph
       with exn ->
-        debug_print 
-          (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
-                         (CicPp.ppterm hetype)
-                         (CicPp.ppterm hetype')
-                         (CicMetaSubst.ppmetasenv [] metasenv)
-                         (CicMetaSubst.ppsubst subst)));
-        raise exn
-
+       enrich localization_tbl he
+        ~f:(fun _ ->
+          (lazy ("The term " ^
+            CicMetaSubst.ppterm_in_context subst he
+             context ^ "(that has type " ^
+            CicMetaSubst.ppterm_in_context subst hetype
+             context ^ ") is here applied to " ^
+            string_of_int (List.length tlbody_and_type) ^
+            " arguments that are more than expected"
+             (* "\nReason: " ^ Lazy.force exn*)))) exn
     in
     let rec eat_prods metasenv subst context hetype ugraph =
       function