From 7d496e618f35a17b8432ac3c7205138f03c95fd2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Aug 2017 14:58:46 +0200
Subject: Introducing a quotation for global references.

---
 tests/quot.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 tests/quot.v

(limited to 'tests')

diff --git a/tests/quot.v b/tests/quot.v
new file mode 100644
index 0000000000..c9aa1f9d14
--- /dev/null
+++ b/tests/quot.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+(** Test for quotations *)
+
+Ltac2 ref0 () := reference:(&x).
+Ltac2 ref1 () := reference:(nat).
+Ltac2 ref2 () := reference:(Datatypes.nat).
+Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
+Fail Ltac2 ref () := reference:(And.Me.neither).
-- 
cgit v1.2.3