X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d3a297d43e88b517cec0e9caf4eef32e322896d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=21bf072781c43cbfd3595090fe41f282e01febd2;hpb=ff3bc8b7c911ff19e9335995428351f6c38494e9;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 21bf07278..d3a297d43 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,17 @@ and type_of_aux' metasenv context t ugraph = in match coer with | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotHandled _ -> + let msg e = + 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*)) + in + enrich msg exn | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c ->