diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-06 14:25:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-06 14:25:02 +0000 |
| commit | d14da289de0035552c9a62ca5036be642ca250db (patch) | |
| tree | 921d6e0a589deb6c4a93d6c0fbeab418aef0ad58 /test-suite/success/DHyp.v | |
| parent | c04a214b50698cb8747e4e08fcc5cd52021068ad (diff) | |
Des exemples sérieux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2762 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/DHyp.v')
| -rw-r--r-- | test-suite/success/DHyp.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/DHyp.v b/test-suite/success/DHyp.v index 330c21f01..1358bb239 100644 --- a/test-suite/success/DHyp.v +++ b/test-suite/success/DHyp.v @@ -1,12 +1,12 @@ -HintDestruct Hypothesis a (le O ?) 3 (Inversion H). +HintDestruct Hypothesis h1 (le ? O) 3 [Fun I -> Inversion I ]. -Goal ~(le O (S O)). +Lemma lem1 : ~(le (S O) O). Intro H. DHyp H. Qed. -HintDestruct Conclusion a (le O ?) 3 Constructor. +HintDestruct Conclusion h2 (le O ?) 3 [Constructor]. -Goal (le O O). +Lemma lem2 : (le O O). DConcl. Qed. |