* in the term (for occur check).
*)
val delift :
- #NCic.status ->
+ #NCicEnvironment.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 ->
+ #NCicEnvironment.status ->
NCic.metasenv ->
NCic.substitution ->
int -> int list ->
(* returns the resulting type, the metasenv and the arguments *)
val saturate:
- #NCic.status ->
+ #NCicEnvironment.status ->
?delta:int -> NCic.metasenv -> NCic.substitution ->
NCic.context -> NCic.term -> int ->
NCic.term * NCic.metasenv * NCic.term list
val int_of_out_scope_tag : NCic.meta_attrs -> int
val is_flexible:
- #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool
+ #NCicEnvironment.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool