1 files changed, 10 insertions, 0 deletions
diff --git a/tests/quot.v b/tests/quot.v
index 4fa9c4fa4e..624c4ad0c1 100644
--- a/tests/quot.v
+++ b/tests/quot.v
@@ -14,3 +14,13 @@ let x := constr:(I) in
 let y := constr:((fun z => z) $x) in
 Control.refine (fun _ => y).
 Qed.
+
+Goal True.
+Proof.
+(** Here, Ltac2 should not put its variables in the same environment as
+    Ltac1 otherwise the second binding fails as x is bound but not an
+    ident. *)
+let x := constr:(I) in
+let y := constr:((fun x => x) $x) in
+Control.refine (fun _ => y).
+Qed.