Fix #12011 ssreflect "rewrite in" with setoids

ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"

Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12011.v b/test-suite/bugs/closed/bug_12011.v
new file mode 100644
index 0000000000..f149b4e8ae
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12011.v
@@ -0,0 +1,21 @@
+From Coq Require Import Setoid ssreflect.
+
+Lemma test A (R : relation A) `{Equivalence _ R} (x y z : A) :
+  R x y -> R y z -> R x z.
+Proof.
+  intros Hxy Hyz.
+  rewrite -Hxy in Hyz.
+  exact Hyz.
+Qed.
+
+
+
+Axiom envs_lookup_delete : bool.
+Axiom envs_lookup_delete_Some : envs_lookup_delete = true <-> False.
+
+Goal envs_lookup_delete = true -> False.
+Proof.
+intros Hlookup.
+rewrite envs_lookup_delete_Some in Hlookup *. (* <- used to revert Hlookup *)
+exact Hlookup.
+Qed.