(* $Id$ *)
val whd :
- ?delta:int -> ?subst:NCic.substitution ->
+ ?delta:int -> subst:NCic.substitution ->
NCic.context -> NCic.term ->
NCic.term
val set_get_relevance :
- (subst:NCic.substitution ->
+ (metasenv:NCic.metasenv -> subst:NCic.substitution ->
NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit
val are_convertible :
- ?subst:NCic.substitution ->
+ metasenv:NCic.metasenv -> subst:NCic.substitution ->
NCic.context -> NCic.term -> NCic.term -> bool
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