From 0cb04b50bfde83001e59cd74da77142b567706d9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 26 Feb 2021 17:35:31 +0100
Subject: 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.
---
 test-suite/bugs/closed/bug_12011.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12011.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3