diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-15 18:06:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-15 18:06:18 +0000 |
| commit | ceba05fb3df673f8378e63c709aff7811014855c (patch) | |
| tree | 141197b03c79b97db581f0e5cfb2c9cb50c0e30d /test-suite | |
| parent | 2e1e80b173846c8ed7ac94ce5f533ffc6cd6c8bd (diff) | |
Réparation absence d'interprétation des liaisons vers listes
d'occurrences (clause "at") dans ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9648 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltac.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 05a6a70f3..880b5da11 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -188,3 +188,13 @@ Ltac to_exist := Goal forall x y : nat, x = y. to_exist. exact (fun H => H). Abort. + +(* Used to fail in V8.1 *) + +Tactic Notation "test" constr(t) integer(n) := + set (k := t) in |- * at n. + +Goal forall x : nat, x = 1 -> x + x + x = 3. +intros x H. +test x 2. +Abort. |