Fix #7812

1 files changed, 30 insertions, 0 deletions

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.