(* $Id$ *)
val whd :
- ?delta:int -> ?subst:NCic.substitution ->
+ ?delta:int -> subst:NCic.substitution ->
NCic.context -> NCic.term ->
NCic.term
(* performs head beta/(delta)/cast reduction; the default is to not perform
delta reduction; if provided, ~upto is the maximum number of beta redexes
reduced *)
-val head_beta_reduce: ?delta:int -> ?upto:int -> NCic.term -> NCic.term
+val head_beta_reduce:
+ ?delta:int -> ?upto:int -> ?subst:NCic.substitution -> NCic.term -> NCic.term
type stack_item
type environment_item