* in the term (for occur check).
*)
val delift :
+ #NCic.status ->
unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
additional (i.e. l' does not intersects l) positions whose restriction was
forced because of type dependencies *)
val restrict:
+ #NCic.status ->
NCic.metasenv ->
NCic.substitution ->
int -> int list ->
(* returns the resulting type, the metasenv and the arguments *)
val saturate:
+ #NCic.status ->
?delta:int -> NCic.metasenv -> NCic.substitution ->
NCic.context -> NCic.term -> int ->
NCic.term * NCic.metasenv * NCic.term list
val is_out_scope_tag : NCic.meta_attrs -> bool
val int_of_out_scope_tag : NCic.meta_attrs -> int
-val is_flexible : NCic.context -> subst:NCic.substitution -> NCic.term -> bool
+val is_flexible:
+ #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool