]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/introductionTactics.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / introductionTactics.ml
index f6283cf680644e6bb9db6413d1d3bf746a7fe816..6bf8ab6c1e37d339c37ac5afaef982fe148c3ea1 100644 (file)
@@ -35,7 +35,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)