diff options
| author | herbelin | 2005-09-08 15:47:01 +0000 |
|---|---|---|
| committer | herbelin | 2005-09-08 15:47:01 +0000 |
| commit | 8899695b2d5f8fe642a806d49fadfac8321b13b4 (patch) | |
| tree | d36e37a143c8ec8e696e9a5b25fd327501a7e456 | |
| parent | 509ea7432afe08d0b342ba31ea7ea3423982c1bc (diff) | |
Test clear final dans intros pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7356 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/intros.v8 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/intros.v8 b/test-suite/success/intros.v8 new file mode 100644 index 0000000000..1da947b50c --- /dev/null +++ b/test-suite/success/intros.v8 @@ -0,0 +1,6 @@ +(* Thinning introduction hypothesis must be done after all introductions *) +(* Submitted by Guillaume Melquiond (bug #1000) *) + +Goal forall A, A -> True. +intros _ _. + |