From fe49db8833803f87e2f750b698f28868d276bfe6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 4 Jun 2019 12:57:16 +0000
Subject: [Ltac2] Interpretation scopes in “constr” arguments of tactic
 notations

---
 test-suite/ltac2/notations.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/ltac2/notations.v

(limited to 'test-suite')

diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v
new file mode 100644
index 0000000000..3d2a875e38
--- /dev/null
+++ b/test-suite/ltac2/notations.v
@@ -0,0 +1,24 @@
+From Ltac2 Require Import Ltac2.
+From Coq Require Import ZArith String List.
+
+Open Scope Z_scope.
+
+Check 1 + 1 : Z.
+
+Ltac2 Notation "ex" arg(constr(nat,Z)) := arg.
+
+Check (1 + 1)%nat%Z = 1%nat.
+
+Lemma two : nat.
+  refine (ex (1 + 1)).
+Qed.
+
+Import ListNotations.
+Close Scope list_scope.
+
+Ltac2 Notation "sl" arg(constr(string,list)) := arg.
+
+Lemma maybe : list bool.
+Proof.
+  refine (sl ["left" =? "right"]).
+Qed.
-- 
cgit v1.2.3