Merge branch 'v8.6' into trunk

6 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5435.v b/test-suite/bugs/closed/5435.v
new file mode 100644
index 000000000..60ace5ce9
--- /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 000000000..50221cdd8
--- /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 000000000..fce671c75
--- /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 000000000..5b3984b6d
--- /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).
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 52acad746..837f2efd0 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -121,6 +121,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
 Check |- {{ 0 }} 0.
 
 (* Check parsing of { and } is not affected by notations #3479 *)
@@ -135,3 +136,9 @@ Notation "" := (@nil) (only printing).
 
 (* Check that a notation cannot be neither parsing nor printing. *)
 Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
+
+(* 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).
diff --git a/test-suite/success/all-check.v b/test-suite/success/all-check.v
new file mode 100644
index 000000000..391bc540e
--- /dev/null
+++ b/test-suite/success/all-check.v
@@ -0,0 +1,3 @@
+Goal True.
+Fail all:Check _.
+Abort.