aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_util.ml47
-rw-r--r--grammar/q_util.mli1
-rw-r--r--intf/extend.mli2
-rw-r--r--ltac/tacentries.ml6
-rw-r--r--parsing/pcoq.ml7
-rw-r--r--plugins/setoid_ring/g_newring.ml418
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:");
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 03:31:02 +0000