From c3efcc501e140a74a948513a0e45223e4d5b521c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Jun 2019 15:08:51 +0200
Subject: Adding the ability to transfer Ltac2 variables to Ltac1 quotations.

---
 test-suite/ltac2/compat.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 489fa638e4..a24c9af10d 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -27,6 +27,22 @@ Fail Ltac2 bar nay := ltac1:(discriminate nay).
 Fail Ltac2 pose1 (v : constr) :=
   ltac1:(pose $v).
 
+(** Variables explicitly crossing the boundary must satisfy typing properties *)
+Goal True.
+Proof.
+(* Missing variable *)
+Fail ltac1:(x |- idtac).
+(* Wrong type *)
+Fail let x := 0 in ltac1:(x |- idtac).
+(* OK, and runtime has access to variable *)
+let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x).
+
+(* Same for ltac1val *)
+Fail Ltac1.run ltac1val:(x |- idtac).
+Fail let x := 0 in Ltac1.run ltac1val:(x |- idtac).
+let x := Ltac1.of_constr constr:(Type) in Ltac1.run ltac1val:(x |- idtac x).
+Abort.
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
-- 
cgit v1.2.3


From e5c788f9efce9a9dd11910cd53c4a99451c48d8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 9 Jun 2019 12:19:28 +0200
Subject: Give a functional type to Ltac1 quotations with a context.

This looks more principled, and doesn't require as much tinkering with
the typing implementation.
---
 test-suite/ltac2/compat.v | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index a24c9af10d..9c11d19c27 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -30,17 +30,14 @@ Fail Ltac2 pose1 (v : constr) :=
 (** Variables explicitly crossing the boundary must satisfy typing properties *)
 Goal True.
 Proof.
-(* Missing variable *)
-Fail ltac1:(x |- idtac).
 (* Wrong type *)
-Fail let x := 0 in ltac1:(x |- idtac).
+Fail ltac1:(x |- idtac) 0.
 (* OK, and runtime has access to variable *)
-let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x).
+ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)).
 
 (* Same for ltac1val *)
-Fail Ltac1.run ltac1val:(x |- idtac).
-Fail let x := 0 in Ltac1.run ltac1val:(x |- idtac).
-let x := Ltac1.of_constr constr:(Type) in Ltac1.run ltac1val:(x |- idtac x).
+Fail Ltac1.run (ltac1val:(x |- idtac) 0).
+Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
 Abort.
 
 (** Test calls to Ltac2 from Ltac1 *)
-- 
cgit v1.2.3