match exn with
RefineFailure msg -> RefineFailure (f msg)
| Uncertain msg -> Uncertain (f msg)
+ | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
| Sys.Break -> raise exn
- | _ -> assert false in
+ | _ -> prerr_endline (Printexc.to_string exn); assert false
+ in
let loc =
try
Cic.CicHash.find localization_tbl t
exn ->
enrich localization_tbl te'
~f:(fun _ ->
- lazy ("The term " ^
+ lazy ("(3)The term " ^
CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
in
(match boh with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl t
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(4)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| CoercGraph.NotMetaClosed ->
enrich localization_tbl t
(Uncertain
- (lazy ("The term " ^
+ (lazy ("(5)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| None ->
enrich localization_tbl t
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(6)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv
subst t context ^
" is not a type since it has type " ^
in
match boh with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl s'
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(7)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| CoercGraph.NotMetaClosed ->
enrich localization_tbl s'
(Uncertain
- (lazy ("The term " ^
+ (lazy ("(8)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
| None ->
enrich localization_tbl s'
(RefineFailure
- (lazy ("The term " ^
+ (lazy ("(9)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context ~metasenv
expected_type' actual_type ugraph2
with
exn ->
+ prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
+ prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(10)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
exn ->
enrich localization_tbl constructor'
~f:(fun _ ->
- lazy ("The term " ^
+ lazy ("(11)The term " ^
CicMetaSubst.ppterm_in_context metasenv subst p'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv subst actual_type
exn ->
enrich localization_tbl p exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(12)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance'
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(13)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(14)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
| CoercGraph.NoCoercion
| CoercGraph.NotMetaClosed
| CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
match
HExtlib.list_findopt
in
(match coer with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl hete exn
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(15)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
| CoercGraph.NotMetaClosed ->
enrich localization_tbl hete exn
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(16)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
| None ->
enrich localization_tbl hete
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(1)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
| exn ->
enrich localization_tbl hete
~f:(fun _ ->
- (lazy ("The term " ^
+ (lazy ("(2)The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst hety
let con_context =
List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
(* second phase: we fix only the constructors *)
+ let saved_menv = metasenv in
let metasenv,ugraph,tys =
List.fold_right
(fun (name,b,ty,cl) (metasenv,ugraph,res) ->
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
- metasenv,ugraph,(name,ty')::res
+ metasenv@saved_menv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
in
metasenv,ugraph,(name,b,ty,cl')::res