aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorHugo Herbelin2019-11-16 11:03:49 +0100
committerHugo Herbelin2020-05-06 17:04:11 +0200
commit86cdd51c4e25fceb12854863419fbdc3f19e44aa (patch)
tree33f0253d75c4ec8aa0166e25226bdbf041a5c703 /plugins
parent986bfd1ff69231f1b17efda2fa5d13b88a39caee (diff)
Stop keeping outdated static list of keywords.
The real list is computed by tok_using in CLexer.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/g_tactic.mlg3
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 6a158bde17..e51b1f051d 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -30,9 +30,6 @@ open Pcoq
let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
-let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter CLexer.add_keyword tactic_kw
-
let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)