2 files changed, 49 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v
new file mode 100644
index 0000000000..4e416778a9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12045.v
@@ -0,0 +1,19 @@
+(* Check enough reduction happens in the conclusion of an induction scheme *)
+
+Lemma foo :
+  forall (P : nat -> Prop),
+    (forall n, P (S n)) ->
+    forall n,
+      (fun e =>
+         IsSucc e ->
+         P e) n.
+Proof.
+Admitted.
+
+Theorem bar : forall n,
+    IsSucc n ->
+    True.
+Proof.
+  intros.
+  Fail induction n using foo. (* was an anomaly *)
+Admitted.
diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v
new file mode 100644
index 0000000000..a714eea81d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7812.v
@@ -0,0 +1,30 @@
+Module Foo.
+  Definition binary A := A -> A -> Prop.
+
+  Definition inter A (R1 R2 : binary A): binary A :=
+    fun (x y:A) => R1 x y /\ R2 x y.
+End Foo.
+
+Module Simple_sparse_proof.
+  Parameter node : Type.
+  Parameter graph : Type.
+  Parameter has_edge : graph -> node -> node -> Prop.
+  Implicit Types x y z : node.
+  Implicit Types G : graph.
+
+  Parameter mem : forall A, A -> list A -> Prop.
+  Hypothesis mem_nil : forall x, mem node x nil = False.
+
+  Definition notin (l: list node): node -> node -> Prop :=
+    fun x y => ~ mem node x l /\ ~ mem node y l.
+
+  Definition edge_notin G l : node -> node -> Prop :=
+    Foo.inter node (has_edge G) (notin l).
+
+  Hint Unfold Foo.inter notin edge_notin : rel_crush.
+
+  Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y.
+  Proof.
+    intros. autounfold with rel_crush. rewrite !mem_nil. tauto.
+  Qed.
+End Simple_sparse_proof.