Getting rid of the "_mods" parsing entry.

It was only used by setoid_ring for the Add Ring command, and was easily
replaced by a dedicated argument. Moreover, it was of no use to tactic
notations.

6 files changed, 15 insertions, 26 deletions

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 53e1f008d..c529260e9 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -22,7 +22,6 @@ type user_symbol =
 | Ulist0 of user_symbol
 | Ulist0sep of user_symbol * string
 | Uopt of user_symbol
-| Umodifiers of user_symbol
 | Uentry of string
 | Uentryl of string * int
 
@@ -68,7 +67,6 @@ let rec mlexpr_of_prod_entry_key f = function
   | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
   | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
   | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
   | Uentry e -> <:expr< Extend.Aentry $f e$ >>
   | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
@@ -77,7 +75,7 @@ let rec mlexpr_of_prod_entry_key f = function
     else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
-| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
+| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
   ListArgType (type_of_user_symbol s)
 | Uopt s ->
   OptArgType (type_of_user_symbol s)
@@ -113,9 +111,6 @@ let rec parse_user_entry s sep =
   else if l > 4 && coincide s "_opt" (l-4) then
     let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
     Uopt entry
-  else if l > 5 && coincide s "_mods" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
-    Umodifiers 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
     Uentryl ("tactic", n)
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 8c437b42a..a34fc0bcb 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -20,7 +20,6 @@ type user_symbol =
 | Ulist0 of user_symbol
 | Ulist0sep of user_symbol * string
 | Uopt of user_symbol
-| Umodifiers of user_symbol
 | Uentry of string
 | Uentryl of string * int
 
diff --git a/intf/extend.mli b/intf/extend.mli
index e1520dec5..10713745e 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -59,7 +59,6 @@ type user_symbol =
 | Ulist0 : user_symbol -> user_symbol
 | Ulist0sep : user_symbol * string -> user_symbol
 | Uopt : user_symbol -> user_symbol
-| Umodifiers : user_symbol -> user_symbol
 | Uentry : string -> user_symbol
 | Uentryl : string * int -> user_symbol
 
@@ -83,7 +82,6 @@ type ('self, 'a) symbol =
 | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
 | Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol
 | Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
-| Amodifiers : ('self, 'a) symbol -> ('self, 'a list) symbol
 | Aself : ('self, 'self) symbol
 | Anext : ('self, 'self) symbol
 | Aentry : 'a Entry.t -> ('self, 'a) symbol
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 99c2213e1..ced473343 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -79,9 +79,6 @@ let rec parse_user_entry s sep =
   else if l > 4 && coincide s "_opt" (l-4) then
     let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
     Uopt entry
-  else if l > 5 && coincide s "_mods" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
-    Umodifiers 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
     Uentryl ("tactic", n)
@@ -110,9 +107,6 @@ let interp_entry_name up_level s sep =
   | Uopt e ->
     let EntryName (t, g) = eval e in
     EntryName (arg_opt t, Aopt g)
-  | Umodifiers e ->
-    let EntryName (t, g) = eval e in
-    EntryName (arg_list t, Amodifiers g)
   | Uentry s ->
     begin
       try try_get_entry uprim s with Not_found ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 75144addb..802c24eef 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -683,13 +683,6 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Alist0sep (s,sep) ->
       Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
   | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
-  | Amodifiers s ->
-       Gram.srules'
-        [([], Gram.action (fun _loc -> []));
-         ([gram_token_of_string "(";
-           Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string ",");
-           gram_token_of_string ")"],
-	   Gram.action (fun _ l _ _loc -> l))]
   | Aself -> Symbols.sself
   | Anext -> Symbols.snext
   | Aentry e ->
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index cd1d704dd..1ebb6e6b7 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -51,9 +51,14 @@ VERNAC ARGUMENT EXTEND ring_mod
   | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ]
 END
 
+VERNAC ARGUMENT EXTEND ring_mods
+  | [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> [ mods ]
+END
+
 VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
-  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
-    [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
+  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
+    [ let l = match l with None -> [] | Some l -> l in
+      let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
       add_theory id (ic t) set k cst (pre,post) power sign div]
   | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
     msg_notice (strbrk "The following ring structures have been declared:");
@@ -75,9 +80,14 @@ VERNAC ARGUMENT EXTEND field_mod
   | [ "completeness" constr(inj) ] -> [ Inject inj ]
 END
 
+VERNAC ARGUMENT EXTEND field_mods
+  | [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> [ mods ]
+END
+
 VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
-| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
-  [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
+| [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
+  [ let l = match l with None -> [] | Some l -> l in
+    let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
 | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
     msg_notice (strbrk "The following field structures have been declared:");