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 _ ->