diff options
| -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 1358bb2399..73907bc4ad 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. +]. |