From 74b37f2429b92ce097100d6af221f273bd2ec9ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Mon, 21 Jun 2021 15:04:34 +0200
Subject: [PATCH] Adding a test for the issue encountered in #14253.

---
 test-suite/success/rewrite_closed.v | 42 +++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 test-suite/success/rewrite_closed.v

diff --git a/test-suite/success/rewrite_closed.v b/test-suite/success/rewrite_closed.v
new file mode 100644
index 0000000000000..98d6bc3cc2fc2
--- /dev/null
+++ b/test-suite/success/rewrite_closed.v
@@ -0,0 +1,42 @@
+From Coq Require Import Setoid Morphisms.
+
+Axiom lattice_for : Type -> Type.
+Axiom constant : forall {T : Type}, T -> lattice_for T.
+
+Axiom lattice_for_rect :
+forall [T : Type] (P : Type), (forall t : T, P) -> forall l : lattice_for T, P.
+
+#[local]
+Declare Instance lattice_for_rect_Proper_85 : forall {A},
+  Proper (forall_relation (fun _ => eq) ==> eq ==> Basics.flip Basics.impl)
+           (@lattice_for_rect A Prop) | 3.
+
+Axiom lattice_rewrite :
+  forall (A T T' : Type) (x : T -> T') (c : A -> lattice_for T)
+      (v : lattice_for A),
+    lattice_for_rect T' x (lattice_for_rect (lattice_for T) c v) =
+    lattice_for_rect T' (fun x0 : A => lattice_for_rect T' x (c x0)) v.
+
+Axiom collapse_might_be_empty : bool.
+
+Axiom PosSet : Type.
+Axiom PosSet_inter : PosSet -> PosSet -> PosSet.
+
+Goal
+forall
+  (l2 : lattice_for PosSet)
+  (l0 : lattice_for PosSet),
+  lattice_for_rect Prop
+    (fun x : PosSet =>
+     lattice_for_rect Prop
+       (fun _ : PosSet => True)
+       (lattice_for_rect (lattice_for PosSet)
+          (fun y' : PosSet =>
+           constant
+             (if collapse_might_be_empty then PosSet_inter x y' else y')) l0)) l2
+.
+Proof.
+intros.
+(* This should not capture a variable *)
+Fail rewrite lattice_rewrite.
+Abort.