From db03c10aaafd3c0128a5b7504f14d4b7aaca842e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 01:16:21 +0200
Subject: Implementing Ltac2 antiquotations in constr syntax.

---
 tests/quot.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'tests')

diff --git a/tests/quot.v b/tests/quot.v
index c9aa1f9d14..4fa9c4fa4e 100644
--- a/tests/quot.v
+++ b/tests/quot.v
@@ -7,3 +7,10 @@ Ltac2 ref1 () := reference:(nat).
 Ltac2 ref2 () := reference:(Datatypes.nat).
 Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
 Fail Ltac2 ref () := reference:(And.Me.neither).
+
+Goal True.
+Proof.
+let x := constr:(I) in
+let y := constr:((fun z => z) $x) in
+Control.refine (fun _ => y).
+Qed.
-- 
cgit v1.2.3