From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 18 Feb 2006 14:33:42 +0000 (+0000)
Subject: More refinement errors localized.
X-Git-Tag: make_still_working~7557
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c98aa929224755305e1f9ccf372629291cf7836;p=helm.git

More refinement errors localized.
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 3faee32df..b9c5b0c6a 100644
--- 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