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 /ltac | |
| 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 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 99c2213e19..ced4733433 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 -> |