aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4034.v
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.
*)