diff options
Diffstat (limited to 'ltac/g_ltac.ml4')
| -rw-r--r-- | ltac/g_ltac.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 1bbdb1779..0c25481d8 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -43,8 +43,6 @@ let tactic_mode = Gram.entry_create "vernac:tactic_command" let new_entry name = let e = Gram.entry_create name in - let entry = Entry.create name in - let () = Pcoq.set_grammar entry e in e let selector = new_entry "vernac:selector" |