+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
+;;
+