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.

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.