From d6c5c2a98d703e1659e1a0274af03bf50d13ba00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 26 Mar 2018 21:20:49 +0200
Subject: Tests for part of #7068 and for #7076 (vm/native_compute and return
 predicate).

---
 test-suite/bugs/closed/7068.v | 6 ++++++
 test-suite/bugs/closed/7076.v | 4 ++++
 2 files changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/7068.v
 create mode 100644 test-suite/bugs/closed/7076.v

diff --git a/test-suite/bugs/closed/7068.v b/test-suite/bugs/closed/7068.v
new file mode 100644
index 0000000000..9fadb195bf
--- /dev/null
+++ b/test-suite/bugs/closed/7068.v
@@ -0,0 +1,6 @@
+(* These tests are only about a subset of #7068 *)
+(* The original issue is still open *)
+
+Inductive foo : let T := Type in T := .
+Definition bob1 := Eval vm_compute in foo_rect.
+Definition bob2 := Eval native_compute in foo_rect.
diff --git a/test-suite/bugs/closed/7076.v b/test-suite/bugs/closed/7076.v
new file mode 100644
index 0000000000..0abc88c282
--- /dev/null
+++ b/test-suite/bugs/closed/7076.v
@@ -0,0 +1,4 @@
+(* These calls were raising an anomaly at some time *)
+Inductive A : nat -> id (nat->Type) := .
+Eval vm_compute in fun x => match x in A y z return y = z with end.
+Eval native_compute in fun x => match x in A y z return y = z with end.
-- 
cgit v1.2.3