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/bugs')

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/bugs')

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 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/bugs')

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/bugs')

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