From edb9a5dd11520804d65e9b1e95ca38bb4acbb0e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 16:01:52 +0200
Subject: Lightweight quotation syntax for terms and idents.

---
 src/g_ltac2.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 47def14125..605cb75d66 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -91,6 +91,8 @@ GEXTEND Gram
     [ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n))
       | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
       | id = Prim.qualid -> CTacRef (RelId id)
+      | "@"; id = Prim.ident -> inj_ident !@loc id
+      | "'"; c = Constr.constr -> inj_open_constr !@loc c
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
       | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c
-- 
cgit v1.2.3