diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-13 16:51:24 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-13 16:51:24 +0000 |
commit | 4d36f0a0f95b94724c033c1399e3f3e18bb0bf1a (patch) | |
tree | ec40371807bd5a8a8b365f0b65fdbd72bde5d9ac /test-suite/output/Tactics.out | |
parent | 2f2715e8f4b1ecbee70c1463e5dde34dced3b2fb (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.out | 1 |
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. |