| _,_ ->
raise
(ProofEngineTypes.Fail
- "The term to unfold is not a constant, a variable or a bound variable ")
+ (lazy "The term to unfold is not a constant, a variable or a bound variable "))
in
let appl he tl =
if tl = [] then he else Cic.Appl (he::tl) in
let cannot_delta_expand t =
raise
(ProofEngineTypes.Fail
- ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in
+ (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
let rec hd_delta_beta context tl =
function
Cic.Rel n as t ->
if res = [] then
raise
(ProofEngineTypes.Fail
- ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+ (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
else
res
in