Merge branch 'v8.6' into trunk

4 files changed, 19 insertions, 0 deletions

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.
+
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.
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 }").
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).