+
+ and coerce_to_something t infty expty subst metasenv context exn ugraph =
+ if not !insert_coercions then
+ raise exn
+ else
+ let clean t subst context =
+ CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t)
+ in
+ let infty = clean infty subst context in
+ let expty = clean expty subst context in
+ match infty, expty with
+ | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
+ (* covariant part *)
+ let name_con = Cic.Name "name_con" in
+ let name_t, ty_s_bo, bo =
+ match t with
+ | Cic.Lambda (name, src, bo) -> name, src, bo
+ | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1]
+ in
+ let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
+ let (bo, _), subst, metasenv, ugraph =
+ coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph
+ in
+ (* contravariant part *)
+ let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2)
+ (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn
+ ugraph
+ in
+ let coerced =
+ Cic.Lambda (name_t,src2,
+ CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
+ in
+ (coerced, expty), subst, metasenv, ugraph
+ | _ ->
+ coerce_atom_to_something t infty expty subst metasenv context exn ugraph
+
+ and coerce_atom_to_something t infty expty subst metasenv context exn ugraph =
+ let coer =
+ CoercGraph.look_for_coercion metasenv subst context infty expty
+ in
+ match coer with
+ | CoercGraph.NotMetaClosed ->
+ (match exn with
+ | RefineFailure s -> raise (Uncertain s)
+ | HExtlib.Localized _ -> assert false
+ | _ -> raise exn)
+ | CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
+ | CoercGraph.NotHandled _ ->
+ raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun (metasenv,last,c) ->
+ try
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last t
+ ugraph in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ c ugraph
+ in
+ let newt, newty, subst, metasenv, ugraph =
+ avoid_double_coercion context subst metasenv
+ ugraph newt expty
+ in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety expty ugraph
+ in
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None -> raise exn
+
+ and coerce_to_sort
+ in_source tgt_sort t type_to_coerce subst context metasenv uragph =
+ match CicReduction.whd ~subst:subst context type_to_coerce with
+ | Cic.Meta _ | Cic.Sort _ ->
+ t,type_to_coerce, subst, metasenv, ugraph
+ | src ->
+ let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+ let exn =
+ RefineFailure (lazy ("(7)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context
+ ^ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst src context
+ ^ " that is not a sort"))
+ in
+ try
+ let (t, ty_t), subst, metasenv, ugraph =
+ coerce_to_something t src tgt
+ subst metasenv context exn ugraph
+ in
+ t, ty_t, subst, metasenv, ugraph
+ with exn -> enrich localization_tbl t exn