From 94397f6e022176a29add6369f0a310b1d7decf62 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 15:23:37 +0200
Subject: Pass Ltac2 variables in a dedicated environment for generic
 arguments.

This is a way to hack around the fact that various interpretation functions
rely wrongly on the values of the environment to do nasty tricks. Typically,
the interpretation of terms is broken, as it will fail when there is a bound
variable with the same name as a hypothesis, instead of producing the
hypothesis itself.
---
 tests/quot.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'tests')

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