+exception NotEmbeddable
+
+let not_embeddable status subst context ty =
+ let rec aux = function
+ | NCic.Meta _
+ | NCic.Const _
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Appl l -> List.iter aux l
+ | t ->
+ (* cannot embed a blob term containing metas *)
+ if (NCicUntrusted.metas_of_term status subst context t = [])
+ then ()
+ else raise NotEmbeddable
+ in
+ try aux ty; noprint (lazy ("Embeddable")); false
+ with NotEmbeddable -> debug (lazy ("Not embeddable")); true
+;;
+
+let tooflex (_,l,_,_) =
+ match l with
+ | Terms.Equation (l,r,_,o) ->
+ (match l,r,o with
+ | Terms.Var _, _, (Terms.Incomparable | Terms.Invertible) -> true
+ | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> true
+ | _ -> false)
+ | _ -> false
+;;
+
+let forward_infer_step status metasenv subst context s t ty =