From b0ee377b3d84305cd121bf8495c02ac3adfa85cc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Nov 2005 09:42:08 +0000 Subject: [PATCH] "Localization" of error messages for eat_prods and applications. --- helm/ocaml/cic_unification/cicRefine.ml | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 21bf07278..202fa8cd7 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -42,6 +42,12 @@ in profiler.HExtlib.profile foo () (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; + +let enrich f = + function + RefineFailure msg -> raise (RefineFailure (f msg)) + | Uncertain msg -> raise (Uncertain (f msg)) + | _ -> assert false let rec split l n = match (l,n) with @@ -484,8 +490,16 @@ and type_of_aux' metasenv context t ugraph = ) tl ([],subst',metasenv',ugraph1) in let tl',applty,subst''',metasenv''',ugraph3 = + try eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 + with + exn -> + enrich + (fun msg -> + lazy ("The application " ^ + CicMetaSubst.ppterm_in_context subst'' t context ^ + " is not well typed:\n" ^ Lazy.force msg)) exn in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) @@ -1101,7 +1115,16 @@ and type_of_aux' metasenv context t ugraph = in match coer with | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotHandled _ -> + let msg = + 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) + in + enrich (fun _ -> msg) exn | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c -> -- 2.39.2