X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FintroductionTactics.ml;h=9ed3647c1306370a3aa3096f5489ffab81c15828;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=f6283cf680644e6bb9db6413d1d3bf746a7fe816;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml
index f6283cf68..9ed3647c1 100644
--- a/helm/ocaml/tactics/introductionTactics.ml
+++ b/helm/ocaml/tactics/introductionTactics.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 let fake_constructor_tac ~n (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
@@ -35,7 +37,7 @@ let fake_constructor_tac ~n (proof, goal) =
           PrimitiveTactics.apply_tac 
            ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)))
            (proof, goal)
-      | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
+      | _ -> raise (ProofEngineTypes.Fail (lazy "Constructor: failed"))
 ;;
 
 let constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n)