_ ->
raise
(Fail
- ("The correctness of hypothesis " ^
+ (lazy ("The correctness of hypothesis " ^
string_of_name n ^
" relies on the body of " ^ hyp)
- )
+ ))
in
entry::context
| Some (_,Cic.Def (_,Some _)) -> assert false
_ ->
raise
(Fail
- ("The correctness of the goal relies on the body of " ^
- hyp))
+ (lazy ("The correctness of the goal relies on the body of " ^
+ hyp)))
in
m,canonical_context',ty
| t -> t
with _ ->
raise
(Fail
- ("Hypothesis " ^ string_of_name n ^
- " uses hypothesis " ^ hyp))
+ (lazy ("Hypothesis " ^ string_of_name n ^
+ " uses hypothesis " ^ hyp)))
in
(b, entry::context)
else
) canonical_context (false, [])
in
if not context_changed then
- raise (Fail ("Hypothesis " ^ hyp ^ " does not exist"));
+ raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
CicUniv.empty_ugraph
with _ ->
- raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal"))
+ raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in
m,canonical_context',ty
| t -> t
if CicUtil.exists_meta n metasenv then
(proof, [n])
else
- raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))
+ raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))