Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].

5 files changed, 34 insertions, 21 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 465073b7aa..2cf590b1d8 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -379,24 +379,27 @@ let with_grammar_rule_protection f x =
 
 let ltac_quotations = ref String.Set.empty
 
-let create_ltac_quotation name cast wit e =
+let create_ltac_quotation name cast (e, l) =
   let () =
     if String.Set.mem name !ltac_quotations then
       failwith ("Ltac quotation " ^ name ^ " already registered")
   in
   let () = ltac_quotations := String.Set.add name !ltac_quotations in
+  let entry = match l with
+  | None -> Aentry (name_of_entry e)
+  | Some l -> Aentryl (name_of_entry e, l)
+  in
 (*   let level = Some "1" in *)
   let level = None in
-  let assoc = Some Extend.RightA in
+  let assoc = None in
   let rule =
-    Next (Next (Next (Stop,
+    Next (Next (Next (Next (Next (Stop,
       Atoken (Lexer.terminal name)),
       Atoken (Lexer.terminal ":")),
-      Aentry (name_of_entry e))
-  in
-  let action v _ _ loc =
-    let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in
-    TacArg (loc, arg)
+      Atoken (Lexer.terminal "(")),
+      entry),
+      Atoken (Lexer.terminal ")"))
   in
+  let action _ v _ _ _ loc = cast (loc, v) in
   let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Tactic.tactic_expr None (None, [gram])
+  Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 17524971f2..23eaa64eec 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -62,8 +62,8 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
 
 (** {5 Adding tactic quotations} *)
 
-val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) ->
-  ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit
-(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is,
-    Ltac grammar now accepts arguments of the form ["name" ":" <e>], and
-    generates a generic argument using [f] on the entry parsed by [e]. *)
+val create_ltac_quotation : string ->
+  ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit
+(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
+    Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
+    generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 06675baa7d..e4ca936a69 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -147,13 +147,7 @@ GEXTEND Gram
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
   tactic_arg:
-    [ [ IDENT "uconstr"; ":"; "("; c = Constr.lconstr; ")" -> TacGeneric (genarg_of_uconstr c)
-      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> ConstrMayEval (ConstrTerm c)
-      | IDENT "ltac"; ":"; "("; a = tactic_expr LEVEL "5"; ")" -> arg_of_expr a
-      | IDENT "ltac"; ":"; "("; n = natural; ")" -> TacGeneric (genarg_of_int n)
-      | IDENT "ipattern"; ":"; "("; ipat = simple_intropattern; ")" ->
-        TacGeneric (genarg_of_ipattern ipat)
-      | c = constr_eval -> ConstrMayEval c
+    [ [ c = constr_eval -> ConstrMayEval c
       | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
       | IDENT "type_term"; c=uconstr -> TacPretype c
       | IDENT "numgoals" -> TacNumgoals ] ]
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 74d98176a4..7da6df717e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -19,6 +19,8 @@ open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
 
+(** Basic tactics *)
+
 TACTIC EXTEND reflexivity
   [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
 END
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 8f336cdb30..9946aea82a 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -17,6 +17,20 @@ open Tacinterp
 open Misctypes
 open Locus
 
+(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
+
+let create_generic_quotation name e wit =
+  let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
+  Egramcoq.create_ltac_quotation name inject (e, None)
+
+let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr
+let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr
+let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern
+let () = create_generic_quotation "int" Pcoq.Prim.integer Stdarg.wit_int
+let () =
+  let inject (loc, v) = Tacexpr.Tacexp v in
+  Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+
 (* Rewriting orientation *)
 
 let _ = Metasyntax.add_token_obj "<-"