aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4785.v
blob: c3c97d3f59f408d4b711e1aaa6f9b212136264c0 (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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
Require Coq.Lists.List Coq.Vectors.Vector.
Require Coq.Compat.Coq85.

Module A.
Import Coq.Lists.List Coq.Vectors.Vector.
Import ListNotations.
Check [ ]%list : list _.
Import VectorNotations ListNotations.
Delimit Scope vector_scope with vector.
Check [ ]%vector : Vector.t _ _.
Check []%vector : Vector.t _ _.
Check [ ]%list : list _.
Check []%list : list _.

Goal True.
  idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *)
Abort.

Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
Delimit Scope mylist_scope with mylist.
Bind Scope mylist_scope with mylist.
Arguments mynil {_}, _.
Arguments mycons {_} _ _.
Notation " [] " := mynil (compat "8.5") : mylist_scope.
Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
Notation " [ x ] " := (mycons x nil) : mylist_scope.
Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.

Import Coq.Compat.Coq85.
Locate Module VectorNotations.
Import VectorDef.VectorNotations.

Check []%vector : Vector.t _ _.
Check []%mylist : mylist _.
Check [ ]%mylist : mylist _.
Check [ ]%list : list _.
End A.

Module B.
Import Coq.Compat.Coq85.

Goal True.
  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
Abort.
End B.