From db7935f343aa2cb11bd3f8ee5c56112e2e266cd3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 7 Dec 2005 18:59:22 +0000 Subject: [PATCH] The last commit about coercions disactivated localization of errors for eat_prods. Localization restored. --- helm/ocaml/cic_unification/cicRefine.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) 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 -- 2.39.2