diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-02 23:40:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-02 23:40:11 +0000 |
| commit | fe3f4a3df7a422208d86532c24112b8f22065fab (patch) | |
| tree | 527b6a8bda624522a88b2a908e6d6d49cf8538e3 | |
| parent | 0cac1ef26c70290099e5072b76591a3c77f250fa (diff) | |
test de la bonne position des vars de ltac entre les vars et les rels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6664 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/ltac.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index abb1c1090..5cd397067 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -110,3 +110,10 @@ Qed. *) +(* Check the precedences of rel context, ltac context and vars context *) +(* (was wrong in V8.0) *) + +Tactic Definition check_binding y := Cut (([y]y) = S). +Goal True. +check_binding true. +Abort. |