X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=2c641fd84f9ee3e48d625951bc970d35a61ed4e2;hb=9e8c5d2163e701413517153f00a52dac1cd31ecd;hp=99c37f8017832625f838c4128fb47cfd046e0bc3;hpb=c56a4b2bad2b1332bc2eda646c18ac547c4ce102;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 99c37f801..2c641fd84 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -67,10 +67,10 @@ let clearbody ~hyp =
                        _ ->
                          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
@@ -84,8 +84,8 @@ let clearbody ~hyp =
                 _ ->
                  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
@@ -129,8 +129,8 @@ let clear ~hyp =
                           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
@@ -138,13 +138,13 @@ let clear ~hyp =
                ) 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
@@ -161,4 +161,4 @@ let set_goal n =
        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))))