in
(match boh with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl t
(RefineFailure
in
match boh with
| CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
| CoercGraph.NotHandled _ ->
enrich localization_tbl s'
(RefineFailure
type_of_aux subst metasenv context expected_type ugraph1
in
let actual_type = CicReduction.whd ~subst context actual_type in
- prerr_endline (CicPp.ppterm expected_type');
- prerr_endline (CicPp.ppterm actual_type);
let subst,metasenv,ugraph3 =
try
fo_unif_subst subst context metasenv
| 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 _ ->
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