X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=3d5626afa4a0a6017346e08537706d3e998adcfe;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=94b5d379d19837cbaa96dd2f722771d13eeb48fc;hpb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 94b5d379d..3d5626afa 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -48,7 +48,7 @@ let fail_tac =
  let fail_tac (proof,goal) =
   let _, metasenv, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
-   raise (Fail "fail tactical")
+   raise (Fail (lazy "fail tactical"))
  in
   mk_tactic fail_tac
 
@@ -118,7 +118,7 @@ let first ~tactics =
               first ~tactics status
         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
       )
-  | [] -> raise (Fail "first: no tactics left")
+  | [] -> raise (Fail (lazy "first: no tactics left"))
  in
   S.mk_tactic (first ~tactics)
 
@@ -140,8 +140,8 @@ let thens ~start ~continuations =
     S.set_goals output_status goals
   with
    Invalid_argument _ -> 
-    let debug = Printf.sprintf "thens: expected %i new goals, found %i"
-     (List.length continuations) (List.length new_goals)
+    let debug = lazy (Printf.sprintf "thens: expected %i new goals, found %i"
+     (List.length continuations) (List.length new_goals))
     in
     raise (Fail debug)
  in
@@ -272,7 +272,7 @@ let solve_tactics ~tactics =
 	  Printexc.to_string e));
          solve_tactics ~tactics status
       )
-  | [] -> raise (Fail "solve_tactics cannot solve the goal");
+  | [] -> raise (Fail (lazy "solve_tactics cannot solve the goal"));
           S.apply_tactic S.id_tac status
  in
   S.mk_tactic (solve_tactics ~tactics)