aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
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 *)