blob: 3f7be4d1c79e0d30e839d6190890806e760ab9cf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
*)
|
