diff options
| author | Pierre-Marie Pédrot | 2016-04-01 11:13:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-01 11:21:39 +0200 |
| commit | b3315a798edcaea533b592cc442e82260502bd49 (patch) | |
| tree | a335abd190d873ca5e4b3e5a737349fc68d2b50f /parsing | |
| parent | 8d272227e4a4b4829678bfb6ecc84673bc47eeb7 (diff) | |
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.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 75144addb2..802c24eef4 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 -> |