3 files changed, 42 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index ce21ff41c3..f41fb5b1e4 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -25,7 +25,7 @@
 # Includes
 ###########################################################################
 
-include ../config/Makefile
+-include ../config/Makefile
 include ../Makefile.common
 
 #######################################################################
diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/7333.v
new file mode 100644
index 0000000000..fba5b9029d
--- /dev/null
+++ b/test-suite/bugs/7333.v
@@ -0,0 +1,39 @@
+Module Example1.
+
+CoInductive wrap : Type :=
+ | item : unit -> wrap.
+
+Definition extract (t : wrap) : unit :=
+match t with
+| item x => x
+end.
+
+CoFixpoint close u : unit -> wrap :=
+match u with
+| tt => item
+end.
+
+Definition table : wrap := close tt tt.
+
+Eval vm_compute in (extract table).
+Eval vm_compute in (extract table).
+
+End Example1.
+
+Module Example2.
+
+Set Primitive Projections.
+CoInductive wrap : Type :=
+ item { extract : unit }.
+
+CoFixpoint close u : unit -> wrap :=
+match u with
+| tt => item
+end.
+
+Definition table : wrap := close tt tt.
+
+Eval vm_compute in (extract table).
+Eval vm_compute in (extract table).
+
+End Example2.
diff --git a/test-suite/bugs/closed/6951.v b/test-suite/bugs/closed/6951.v
new file mode 100644
index 0000000000..419f8d7c4e
--- /dev/null
+++ b/test-suite/bugs/closed/6951.v
@@ -0,0 +1,2 @@
+Record float2 : Set := Float2 { Fnum : unit }.
+Scheme Equality for float2.