diff options
| author | Hugo Herbelin | 2015-10-24 09:57:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-24 10:05:03 +0200 |
| commit | 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 (patch) | |
| tree | 7747e567b36ce6db92154eaeedbe95eaa723c751 /test-suite | |
| parent | d30a7244b52e86c364320a8fa0794c7686f30074 (diff) | |
Backtracking on interpreting toplevel calls to exact in scope determined
by the type to prove (was introduced in 35846ec22, r15978, Nov 2012).
Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.
Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...
See #4034 for a discussion.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4034.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4034.v b/test-suite/bugs/closed/4034.v new file mode 100644 index 0000000000..3f7be4d1c7 --- /dev/null +++ b/test-suite/bugs/closed/4034.v @@ -0,0 +1,25 @@ +(* This checks compatibility of interpretation scope used for exact + between 8.4 and 8.5. See discussion at + https://coq.inria.fr/bugs/show_bug.cgi?id=4034. It is not clear + what we would like exactly, but certainly, if exact is interpreted + in a special scope, it should be interpreted consistently so also + in ltac code. *) + +Record Foo := {}. +Bind Scope foo_scope with Foo. +Notation "!" := Build_Foo : foo_scope. +Notation "!" := 1 : core_scope. +Open Scope foo_scope. +Open Scope core_scope. + +Goal Foo. + Fail exact !. +(* ... but maybe will we want it to succeed eventually if we ever + would be able to make it working the same in + +Ltac myexact e := exact e. + +Goal Foo. + myexact !. +Defined. +*) |