Allowing calls to Ltac2 inside Ltac1.

1 files changed, 56 insertions, 0 deletions

diff --git a/tests/compat.v b/tests/compat.v
new file mode 100644
index 0000000000..44421349da
--- /dev/null
+++ b/tests/compat.v
@@ -0,0 +1,56 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+(** Test calls to Ltac1 from Ltac2 *)
+
+Ltac2 foo () := ltac1:(discriminate).
+
+Goal true = false -> False.
+Proof.
+foo ().
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+(** FIXME when the non-strict mode is implemented. *)
+Fail intros H; ltac1:(rewrite H); reflexivity.
+Abort.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac2 bar nay := ltac1:(discriminate nay).
+
+(** Test calls to Ltac2 from Ltac1 *)
+
+Set Default Proof Mode "Classic".
+
+Ltac foo := ltac2:(foo ()).
+
+Goal true = false -> False.
+Proof.
+ltac2:(foo ()).
+Qed.
+
+Goal true = false -> False.
+Proof.
+foo.
+Qed.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac bar x := ltac2:(foo x).
+
+Ltac mytac tac := idtac "wow".
+
+Goal True.
+Proof.
+(** Fails because quotation is evaluated eagerly *)
+Fail mytac ltac2:(fail).
+(** One has to thunk thanks to the idtac trick *)
+let t := idtac; ltac2:(fail) in mytac t.
+constructor.
+Qed.