Added Decompose tactic

[helm.git] / helm / gTopLevel / introductionTactics.ml

diff --git a/helm/gTopLevel/introductionTactics.ml b/helm/gTopLevel/introductionTactics.ml
index bd29f4f5a147ed59f7f33472725f2ea03aa929e6..bc28c41709c92719a143d40506a9db6860a2f8e5 100644 (file)
--- a/helm/gTopLevel/introductionTactics.ml
+++ b/helm/gTopLevel/introductionTactics.ml
@@ -34,7 +34,7 @@ let constructor_tac ~n ~status:(proof, goal) =
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
          PrimitiveTactics.apply_tac ~status:(proof, goal)
           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
-      | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
+      | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
 ;;