(* this should be moved elsewhere *)
val fix_sorts:
- #NCic.status -> NCic.metasenv -> NCic.substitution ->
+ #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution ->
NCic.term -> NCic.metasenv * NCic.term
(* delift_type_wrt_terms st m s c t args
NCic.metasenv * NCic.substitution * NCic.term
val sortfy :#
- NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context ->
+ NCicEnvironment.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
val debug : bool ref