X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=95e6c7ba6d213ef308592031b32e4e550666d29a;hb=7a7af8e1ed42aa440476975ec918d38f0c3d13c9;hp=e1c1e91cee28838f92891ac72c3e335a65a7ab7a;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e1c1e91ce..95e6c7ba6 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 @@ -1321,7 +1331,9 @@ let typecheck metasenv uri obj ~localization_tbl = let metasenv,ugraph,cl' = List.fold_right (fun (name,ty) (metasenv,ugraph,res) -> - let ty = CicTypeChecker.debrujin_constructor uri typesno ty in + let ty = + CicTypeChecker.debrujin_constructor + ~cb:(relocalize localization_tbl) uri typesno ty in let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in