From 4d5e3f3f00cb1848861b938ba1a57c33800d71a6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Sep 2017 01:59:34 +0200
Subject: Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in
 anomalies.

---
 tests/compat.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tests')

diff --git a/tests/compat.v b/tests/compat.v
index 44421349da..f4e849c5de 100644
--- a/tests/compat.v
+++ b/tests/compat.v
@@ -25,6 +25,9 @@ Abort.
 (** Variables do not cross the compatibility layer boundary. *)
 Fail Ltac2 bar nay := ltac1:(discriminate nay).
 
+Fail Ltac2 pose1 (v : constr) :=
+  ltac1:(pose $v).
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
@@ -54,3 +57,4 @@ Fail mytac ltac2:(fail).
 let t := idtac; ltac2:(fail) in mytac t.
 constructor.
 Qed.
+
-- 
cgit v1.2.3