exception ReferenceToVariable
exception ReferenceToCurrentProof
exception ReferenceToInductiveDefinition
+val ndebug : bool ref
val fdebug : int ref
val whd :
?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term
val normalize:
?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term
-(* performs an head beta/cast reduction; the default is to not perform
- delta reduction *)
-val head_beta_reduce: ?delta:bool -> Cic.term -> Cic.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:bool -> ?upto:int -> Cic.term -> Cic.term