From 8c962c46397d707435834d6765d1c243a844babd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Sep 2013 22:05:27 +0200
Subject: Actually adding the grammar entry to handle tactics in terms.

---
 parsing/g_constr.ml4 | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 51214d91ea..cdaa809d28 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -211,6 +211,9 @@ GEXTEND Gram
 	  CGeneralization (!@loc, Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
 	  CGeneralization (!@loc, Explicit, None, c)
+      | "$("; tac = Tactic.tactic; ")$" ->
+          let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
+          CHole (!@loc, None, Some arg)
       ] ]
   ;
   forall:
-- 
cgit v1.2.3