From cbc3a5f16871adb399689f7673a2a29a82dbf0cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 16:30:40 +0100
Subject: All arguments defined through ARGUMENT EXTEND declare a tactic scope.

Amongs other things, it kind of fixes bug #4492, even though you cannot really
take advantage of the parsed data for now.
---
 CHANGES               | 3 +++
 grammar/argextend.ml4 | 7 +++++--
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index ae055cb2f8..7de1015275 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,9 @@ Tactics
   for which pattern can be omitted, as in regular pattern-matching).
 - Tactic scopes in Ltac like constr: and ltac: now require parentheses around
   their argument.
+- Every generic argument type declares a tactic scope of the form "name:(...)"
+  where name is the name of the argument. This generalizes the constr: and ltac:
+  instances.
 
 Program
 
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 13f7611131..65dc237bb7 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -231,8 +231,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
      <:str_item< do {
       Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule
-        $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$ }
-     >> ]
+        $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$;
+      Egramcoq.create_ltac_quotation $se$
+        (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v))
+        ($lid:s$, None)
+      } >> ]
 
 let declare_vernac_argument loc s pr cl =
   let se = mlexpr_of_string s in
-- 
cgit v1.2.3