aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Tactics.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-17 15:38:40 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-17 15:38:40 +0000
commit473bc54aa1df56b64a6fefb355041e6fa277022b (patch)
tree9cd3dbd7f7f841ae1db46aa9c67fab2e1d7bc326 /test-suite/output/Tactics.v
parent48d0870c093a15faaf3dbb327afa94f5da2a38ea (diff)
Bypassing the use of (currently unimplemented) "Show Script" in tests
that used it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Tactics.v')
-rw-r--r--test-suite/output/Tactics.v13
1 files changed, 4 insertions, 9 deletions
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 8fa919940..a7c497cfa 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -3,16 +3,11 @@
Tactic Notation "a" constr(x) := apply x.
Tactic Notation "e" constr(x) := exact x.
-Lemma test : True -> True /\ True.
-intro H; split; [a H|e H].
-Show Script.
-Qed.
+Ltac f H := split; [a H|e H].
+Print Ltac f.
(* Test printing of match context *)
(* Used to fail after translator removal (see bug #1070) *)
-Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
-Proof.
-intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
-Show Script.
-Qed.
+Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
+Print Ltac g.