From 1a3fc19d1160cb3896e62a16c8e68c97880c748b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 29 Sep 2016 14:00:34 -0400
Subject: Move vector/list compat notations to their relevant files

Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing.  Also update the related test-suite
files.
---
 test-suite/bugs/closed/4733.v           |  8 +++---
 test-suite/bugs/closed/4785.v           |  2 +-
 test-suite/bugs/closed/4785_compat_85.v | 46 +++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/4803.v           | 20 +++++++++++---
 test-suite/success/Notations.v          |  7 ++++-
 5 files changed, 74 insertions(+), 9 deletions(-)
 create mode 100644 test-suite/bugs/closed/4785_compat_85.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
index ac0653492a..a6ebda61cf 100644
--- a/test-suite/bugs/closed/4733.v
+++ b/test-suite/bugs/closed/4733.v
@@ -25,16 +25,16 @@ Check [ _ ]%list : list _.
 Check [ _ ]%vector : Vector.t _ _.
 Check [ _ ; _ ]%list : list _.
 Check [ _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
 
 Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
-(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *)
+(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, this section can also just be removed. *)
 Check [ ]%mylist : mylist _.
 Check [ ]%list : list _.
 Check []%vector : Vector.t _ _.
diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
index 14af2d91df..c3c97d3f59 100644
--- a/test-suite/bugs/closed/4785.v
+++ b/test-suite/bugs/closed/4785.v
@@ -21,7 +21,7 @@ Delimit Scope mylist_scope with mylist.
 Bind Scope mylist_scope with mylist.
 Arguments mynil {_}, _.
 Arguments mycons {_} _ _.
-Notation " [] " := mynil : mylist_scope.
+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.
diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v
new file mode 100644
index 0000000000..9d65840acd
--- /dev/null
+++ b/test-suite/bugs/closed/4785_compat_85.v
@@ -0,0 +1,46 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *)
+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 _.
+Fail Check []%list : list _.
+
+Goal True.
+  idtac; [ ]. (* Note that vector notations 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.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
index 3ca5c095f5..4530548b8f 100644
--- a/test-suite/bugs/opened/4803.v
+++ b/test-suite/bugs/opened/4803.v
@@ -25,10 +25,24 @@ Check [ _ ]%list : list _.
 Check [ _ ]%vector : Vector.t _ _.
 Check [ _ ; _ ]%list : list _.
 Check [ _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *)
+Check [ _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
+
+(** Now check that we can add and then remove notations from the parser *)
+(* We should be able to stick some vernacular here to remove [] from the parser *)
+Fail Remove Notation "[]".
+Goal True.
+  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
+  (* idtac; []. *)
+  constructor.
+Qed.
+
+Check { _ : _ & _ }.
+Reserved Infix "&" (at level 0).
+Fail Remove Infix "&".
+(* Check { _ : _ & _ }. *)
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2f7c62972a..30abd961b1 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -58,7 +58,7 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
 
 (* Check multi-tokens recursive notations *)
 
-Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
+Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).
 Check [ 0 ].
 Check [ 0 # ; 1 ].
 
@@ -110,3 +110,8 @@ Goal True -> True. intros H. exact H. Qed.
 
 (* Check absence of collision on ".." in nested notations with ".." *)
 Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* Check that vector notations do not break Ltac [] (bugs #4785, #4733) *)
+Require Import Coq.Vectors.VectorDef.
+Import VectorNotations.
+Goal True. idtac; []. (* important for test: no space here *) constructor. Qed.
-- 
cgit v1.2.3


From c3b9a7bf9fcd162628ce6a2a544652ca096cfe54 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Oct 2016 16:27:37 +0200
Subject: Fix bug #5145: Anomaly: index to an anonymous variable.

When printing evar constraints, we ensure that every variable from the
rel context has a name.
---
 test-suite/bugs/closed/5145.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/5145.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5145.v b/test-suite/bugs/closed/5145.v
new file mode 100644
index 0000000000..0533d21e0c
--- /dev/null
+++ b/test-suite/bugs/closed/5145.v
@@ -0,0 +1,10 @@
+Class instructions :=
+  {
+    W : Type;
+    ldi : nat -> W
+  }.
+
+Fail Definition foo :=
+  let y2 := ldi 0 in
+  let '(CF, _) := (true, 0) in
+  y2.
-- 
cgit v1.2.3


From 159b10655172b6f0888f9622be3620c3c33d35b1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Oct 2016 12:17:01 +0200
Subject: Test for bug #4874.

---
 test-suite/output/qualification.out |  3 +++
 test-suite/output/qualification.v   | 19 +++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 test-suite/output/qualification.out
 create mode 100644 test-suite/output/qualification.v

(limited to 'test-suite')

diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 0000000000..3cf3c2d8fb
--- /dev/null
+++ b/test-suite/output/qualification.out
@@ -0,0 +1,3 @@
+File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7:
+Error: Signature components for label test do not match: expected type
+"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
new file mode 100644
index 0000000000..d39097e2dd
--- /dev/null
+++ b/test-suite/output/qualification.v
@@ -0,0 +1,19 @@
+Module Type T1.
+  Parameter t : Type.
+End T1.
+
+Module Type T2.
+  Declare Module M : T1.
+  Parameter t : Type.
+  Parameter test : t = M.t.
+End T2.
+
+Module M1 <: T1.
+  Definition t : Type := bool.
+End M1.
+
+Module M2 <: T2.
+  Module M := M1.
+  Definition t : Type := nat.
+  Lemma test : t = t. Proof. reflexivity. Qed.
+End M2.
-- 
cgit v1.2.3


From 502d901fee12f07c31c2ea8b8c1455f74876d986 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Oct 2016 15:55:53 +0200
Subject: Example illustrating non-local inference of the default type of
 impossible branches (see PR #323).

---
 test-suite/success/CaseInClause.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v
index 599b9566cb..6424fe92dd 100644
--- a/test-suite/success/CaseInClause.v
+++ b/test-suite/success/CaseInClause.v
@@ -24,3 +24,6 @@ Theorem foo : forall (n m : nat) (pf : n = m),
 (* Check redundant clause is removed *)
 Inductive I : nat * nat -> Type := C : I (0,0).
 Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end.
+
+(* An example of non-local inference of the type of an impossible case *)
+Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2.
-- 
cgit v1.2.3


From 48b342ed5b9fb514961e10b2684243dc0b4078be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Oct 2016 17:37:15 +0200
Subject: Fix output test for module qualification.

The output was embedding local paths from my machine.
---
 test-suite/output/qualification.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
index 3cf3c2d8fb..9300c3f546 100644
--- a/test-suite/output/qualification.out
+++ b/test-suite/output/qualification.out
@@ -1,3 +1,3 @@
-File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7:
+File "stdin", line 19, characters 0-7:
 Error: Signature components for label test do not match: expected type
 "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
-- 
cgit v1.2.3