Merge branch 'v8.5'

3 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3071.v b/test-suite/bugs/closed/3071.v
index 611ac60655..611ac60655 100644
--- a/test-suite/bugs/opened/3071.v
+++ b/test-suite/bugs/closed/3071.v
diff --git a/test-suite/bugs/closed/3993.v b/test-suite/bugs/closed/3993.v
new file mode 100644
index 0000000000..086d8dd0f3
--- /dev/null
+++ b/test-suite/bugs/closed/3993.v
@@ -0,0 +1,3 @@
+(* Test smooth failure on not fully applied term to destruct with eqn: given *)
+Goal True.
+Fail induction S eqn:H.
diff --git a/test-suite/bugs/closed/4078.v b/test-suite/bugs/closed/4078.v
new file mode 100644
index 0000000000..236cd2fbb1
--- /dev/null
+++ b/test-suite/bugs/closed/4078.v
@@ -0,0 +1,14 @@
+Module Type S.
+
+Axiom foo : nat.
+
+End S.
+
+Module M : S.
+
+Definition bar := 0.
+Definition foo := bar.
+
+End M.
+
+Print All Dependencies M.foo.