* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
exception RefineFailure of string Lazy.t;;
and avoid_double_coercion subst metasenv ugraph t ty =
match t with
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
+ | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
let source_carr = CoercGraph.source_of c2 in
let tgt_carr = CicMetaSubst.apply_subst subst ty in
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
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
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