aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Tactics.out
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-13 16:51:24 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-13 16:51:24 +0000
commit4d36f0a0f95b94724c033c1399e3f3e18bb0bf1a (patch)
treeec40371807bd5a8a8b365f0b65fdbd72bde5d9ac /test-suite/output/Tactics.out
parent2f2715e8f4b1ecbee70c1463e5dde34dced3b2fb (diff)
Correction test-suite suite à r9186
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9238 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Tactics.out')
-rw-r--r--test-suite/output/Tactics.out1
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 365fa9bb4..8e8b8059f 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,5 +1,4 @@
intro H; split; [ a H | e H ].
-
intros; match goal with
| |- context [if ?X then _ else _] => case X
end; trivial.