3 files changed, 45 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12649.v b/test-suite/bugs/closed/bug_12649.v
new file mode 100644
index 0000000000..5547de84ff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12649.v
@@ -0,0 +1,11 @@
+
+
+Module Type A.
+
+  Record baz : Prop := B { }. (* any sort would do *)
+
+End A.
+
+Print A.
+Module Type UseA (c: A). End UseA.
+Print UseA. (* ANOMALY! Int.Map.get's assert false *)
diff --git a/test-suite/success/bug_10890.v b/test-suite/success/bug_10890.v
new file mode 100644
index 0000000000..37b6c816cc
--- /dev/null
+++ b/test-suite/success/bug_10890.v
@@ -0,0 +1,8 @@
+Require Import Derive.
+
+Derive foo SuchThat (foo = foo :> nat) As bar.
+Proof.
+  Unshelve.
+  2:abstract exact 0.
+   exact eq_refl.
+Defined. (* or Qed: anomaly kernel doesn't support existential variables *)
diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v
index 508cc2be7d..eae1b75689 100644
--- a/test-suite/success/sprop_uip.v
+++ b/test-suite/success/sprop_uip.v
@@ -95,6 +95,32 @@ Section funext.
     := eq_refl.
 End funext.
 
+(* test reductions on inverted cases *)
+
+(* first check production of correct blocked cases *)
+Definition lazy_seq_rect := Eval lazy in seq_rect.
+Definition vseq_rect := Eval vm_compute in seq_rect.
+Definition native_seq_rect := Eval native_compute in seq_rect.
+Definition cbv_seq_rect := Eval cbv in seq_rect.
+
+(* check it reduces according to indices *)
+Ltac reset := match goal with H : _ |- _ => change (match H with srefl _ => False end) end.
+Ltac check := match goal with |- False => idtac end.
+Lemma foo (H:seq 0 0) : False.
+Proof.
+  reset.
+  Fail check. (* check that "reset" and "check" actually do something *)
+
+  lazy; check; reset.
+
+  (* TODO *)
+  vm_compute. Fail check.
+  native_compute. Fail check.
+  cbv. Fail check.
+  cbn. Fail check.
+  simpl. Fail check.
+Abort.
+
 (* check that extraction doesn't fall apart on matches with special reduction *)
 Require Extraction.