Moving and enhancing the grammar_tactic_prod_item_expr type.

5 files changed, 28 insertions, 26 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 14a80379ec..ae9328fcc0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -200,10 +200,6 @@ type one_inductive_expr =
 type proof_expr =
   plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
 
-type grammar_tactic_prod_item_expr =
-  | TacTerm of string
-  | TacNonTerm of Loc.t * string * (Names.Id.t * string)
-
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
   | SetLevel of int
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 56f32196b6..fe750f429f 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -385,18 +385,18 @@ VERNAC ARGUMENT EXTEND ltac_production_sep
 END
 
 let pr_ltac_production_item = function
-| TacTerm s -> quote (str s)
-| TacNonTerm (_, arg, (id, sep)) ->
+| Tacentries.TacTerm s -> quote (str s)
+| Tacentries.TacNonTerm (_, (arg, sep), id) ->
   let sep = match sep with
-  | "" -> mt ()
-  | sep -> str "," ++ spc () ++ quote (str sep)
+  | None -> mt ()
+  | Some sep -> str "," ++ spc () ++ quote (str sep)
   in
   str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")"
 
 VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
-| [ string(s) ] -> [ TacTerm s ]
+| [ string(s) ] -> [ Tacentries.TacTerm s ]
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ TacNonTerm (loc, Names.Id.to_string nt, (p, Option.default "" sep)) ]
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ]
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index ced4733433..46e48c6953 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -19,6 +19,10 @@ open Vernacexpr
 open Libnames
 open Nameops
 
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
@@ -60,24 +64,28 @@ let get_tacentry n m =
   else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
   else EntryName (rawwit Constrarg.wit_tactic, atactic n)
 
+let get_separator = function
+| None -> error "Missing separator."
+| Some sep -> sep
+
 let rec parse_user_entry s sep =
   let open Extend in
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    let entry = parse_user_entry (String.sub s 3 (l-8)) None in
     Ulist1 entry
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
-    Ulist1sep (entry, sep)
+    let entry = parse_user_entry (String.sub s 3 (l-12)) None in
+    Ulist1sep (entry, get_separator sep)
   else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    let entry = parse_user_entry (String.sub s 0 (l-5)) None in
     Ulist0 entry
   else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
-    Ulist0sep (entry, sep)
+    let entry = parse_user_entry (String.sub s 0 (l-9)) None in
+    Ulist0sep (entry, get_separator sep)
   else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    let entry = parse_user_entry (String.sub s 0 (l-4)) None in
     Uopt entry
   else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
     let n = Char.code s.[6] - 48 in
@@ -208,7 +216,7 @@ let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
 
 let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, nt, (_, sep)) ->
+  | TacNonTerm (loc, (nt, sep), _) ->
       let EntryName (etyp, e) = interp_entry_name lev nt sep in
       GramNonTerminal (loc, etyp, e)
 
@@ -284,7 +292,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
 
 let cons_production_parameter = function
 | TacTerm _ -> None
-| TacNonTerm (_, _, (id, _)) -> Some id
+| TacNonTerm (_, _, id) -> Some id
 
 let add_tactic_notation (local,n,prods,e) =
   let ids = List.map_filter cons_production_parameter prods in
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index b60d8f478e..0f4bb2530e 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -9,10 +9,14 @@
 open Vernacexpr
 open Tacexpr
 
+type 'a grammar_tactic_prod_item_expr =
+| TacTerm of string
+| TacNonTerm of Loc.t * 'a * Names.Id.t
+
 (** Adding a tactic notation in the environment *)
 
 val add_tactic_notation :
-  locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
+  locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr ->
     unit
 
 val add_ml_tactic_notation : ml_tactic_name ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9054ba0b67..f0548238a7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -104,12 +104,6 @@ module Make
     if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
     else id
 
-  let pr_production_item = function
-    | TacNonTerm (loc, nt, (p, sep)) ->
-      let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
-      str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
-    | TacTerm s -> qs s
-
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s