diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-27 21:33:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-27 21:33:12 +0000 |
| commit | 7e3405afba3eafd55c42e5f55b31591428eb74b6 (patch) | |
| tree | ff117350436b2f34903815797a2e8d922f80ea25 /test-suite/success/DHyp.v | |
| parent | 5670cc17f6bfc5b6757f9f950c55c267abe1c818 (diff) | |
Suppression en v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5156 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/DHyp.v')
| -rw-r--r-- | test-suite/success/DHyp.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/DHyp.v b/test-suite/success/DHyp.v index 1358bb239..73907bc4a 100644 --- a/test-suite/success/DHyp.v +++ b/test-suite/success/DHyp.v @@ -1,3 +1,4 @@ +V7only [ HintDestruct Hypothesis h1 (le ? O) 3 [Fun I -> Inversion I ]. Lemma lem1 : ~(le (S O) O). @@ -10,3 +11,4 @@ HintDestruct Conclusion h2 (le O ?) 3 [Constructor]. Lemma lem2 : (le O O). DConcl. Qed. +]. |