+ t orig_t ty `XTSort exn
+
+and force_to_inductive status metasenv subst context t orig_t localise ty =
+ try
+ let metasenv, subst, ty =
+ NCicUnification.indfy status (Failure "indfy") metasenv subst context ty in
+ metasenv, subst, t, ty
+ with
+ Failure _ ->
+ let msg =
+ (lazy (localise orig_t,
+ "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+ " is not a (co)inductive type: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
+ let ty = NCicReduction.whd status ~subst context ty in
+(* prerr_endline ("#### " ^ status#ppterm ~metasenv ~subst ~context ty); *)
+ let exn =
+ if NCicUnification.could_reduce status ~subst context ty then
+ Uncertain msg
+ else
+ RefineFailure msg
+ in
+ raise exn
+(* FG: this should be as follows but the case `XTInd is not imp;emented yet
+ try_coercions status ~localise metasenv subst context
+ t orig_t ty `XTInd exn
+*)