type machine = int * environment_item list * NCic.term * stack_item list
val reduce_machine :
- delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> machine
+ delta:int -> ?subst:NCic.substitution -> NCic.context -> machine ->
+ machine * bool
val from_stack : stack_item -> machine
val unwind : machine -> NCic.term