From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 Dec 2005 18:59:22 +0000 (+0000)
Subject: The last commit about coercions disactivated localization of errors for
X-Git-Tag: make_still_working~8035
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=db7935f343aa2cb11bd3f8ee5c56112e2e266cd3;p=helm.git

The last commit about coercions disactivated localization of errors for
eat_prods. Localization restored.
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e1c1e91ce..20be9363b 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1087,7 +1087,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                          let c_s = carr s subst context in 
                          CoercGraph.look_for_coercion c_hety c_s, c_s
                        in
-                       match coer with
+                       (match coer with
                        | CoercGraph.NoCoercion 
                        | CoercGraph.NotHandled _ ->
                            enrich localization_tbl hete
@@ -1115,7 +1115,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                               subst metasenv ugraph 
                                 (Cic.Appl[c;hete]) tgt_carr
                            in
-                            newt, subst, metasenv, ugraph
+                            newt, subst, metasenv, ugraph)
+                     | exn ->
+                        enrich localization_tbl hete
+                         ~f:(fun _ ->
+                           (lazy ("The term " ^
+                             CicMetaSubst.ppterm_in_context subst hete
+                              context ^ " has type " ^
+                             CicMetaSubst.ppterm_in_context subst hety
+                              context ^ " but is here used with type " ^
+                             CicMetaSubst.ppterm_in_context subst s context
+                              (* "\nReason: " ^ Lazy.force e*)))) exn
                    in
                    let coerced_args,metasenv',subst',t',ugraph2 =
                      eat_prods metasenv subst context