From fedc831df9626a31cd0d26ee6b9e022b67f90c2a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Feb 2017 14:34:44 +0100
Subject: Fixing a little bug in using the "where" clause for inductive types.

This was not working when the inductive type had implicit parameters.

This could still be improved. E.g. the following still does not work:

Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.

But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
---
 test-suite/success/Notations.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 511b60b4bb..8c83b196e4 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -116,3 +116,9 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
+(* Check "where" clause for inductive types with parameters *)
+
+Reserved Notation "x === y" (at level 50).
+Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
+ where "x === y" := (EQ x y).
-- 
cgit v1.2.3


From 70bcfcf5b2ea485ebe253158c37b89dfac63820b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 4 Apr 2017 10:44:15 +0200
Subject: Test file for #5435:  [Eval native_compute in] raises anomaly.

---
 test-suite/bugs/closed/5435.v | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 test-suite/bugs/closed/5435.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5435.v b/test-suite/bugs/closed/5435.v
new file mode 100644
index 0000000000..60ace5ce96
--- /dev/null
+++ b/test-suite/bugs/closed/5435.v
@@ -0,0 +1,2 @@
+Definition foo (x : nat) := Eval native_compute in x.
+
-- 
cgit v1.2.3


From 007ab31b4d1b9457d2758a614aed5a49dee53b62 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Apr 2017 18:35:03 +0200
Subject: Fixing #5460 (limitation in computing deps in pattern-matching
 compilation).

This was assuming dependencies occurring in configurations of
the form x:A, y:B x, z:C x y |- match x, y, z with ... end".

But still work to do for better management of dependencies in general...
---
 test-suite/bugs/closed/5460.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/5460.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5460.v b/test-suite/bugs/closed/5460.v
new file mode 100644
index 0000000000..50221cdd83
--- /dev/null
+++ b/test-suite/bugs/closed/5460.v
@@ -0,0 +1,11 @@
+(* Bugs in computing dependencies in pattern-matching compilation *)
+
+Inductive A := a1 | a2.
+Inductive B := b.
+Inductive C : A -> Type := c : C a1 | d : C a2.
+Definition P (x : A) (y : C x) (z : B) : nat :=
+  match z, x, y with
+      | b, a1, c => 0
+      | b, a2, d => 0
+      | _, _, _ => 1
+  end.
-- 
cgit v1.2.3


From e73b124a9d504e1759d4a4a0d3899882f58d459a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 16:12:58 +0200
Subject: Fix anomaly when doing [all:Check _.] during a proof.

---
 test-suite/success/all-check.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/success/all-check.v

(limited to 'test-suite')

diff --git a/test-suite/success/all-check.v b/test-suite/success/all-check.v
new file mode 100644
index 0000000000..391bc540e4
--- /dev/null
+++ b/test-suite/success/all-check.v
@@ -0,0 +1,3 @@
+Goal True.
+Fail all:Check _.
+Abort.
-- 
cgit v1.2.3


From 53a50875b28ad96ab1559ca3f97db5133ca5c78e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Apr 2017 23:30:44 +0200
Subject: Fixing bug #5469 (notation format not recognizing curly braces).

---
 test-suite/bugs/closed/5469.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/5469.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v
new file mode 100644
index 0000000000..fce671c754
--- /dev/null
+++ b/test-suite/bugs/closed/5469.v
@@ -0,0 +1,3 @@
+(* Some problems with the special treatment of curly braces *)
+
+Reserved Notation "'a' { x }" (at level 0, format "'a' { x }").
-- 
cgit v1.2.3


From 727ef1bd345f9ad9e08d9e4f136e2db7d034a93d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Apr 2017 22:35:38 +0200
Subject: Fixing bug #5470 (anomaly on notations with misused "binder" type).

---
 test-suite/bugs/closed/5470.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/5470.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5470.v b/test-suite/bugs/closed/5470.v
new file mode 100644
index 0000000000..5b3984b6df
--- /dev/null
+++ b/test-suite/bugs/closed/5470.v
@@ -0,0 +1,3 @@
+(* This used to raise an anomaly *)
+
+Fail Reserved Notation "x +++ y" (at level 70, x binder).
-- 
cgit v1.2.3