diff options
| -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. |