From 2ca8fd3597cdb7fc2e45d6df1c81e03bef9e8827 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 22 Nov 2020 11:45:41 -0800
Subject: Remove unused parsing code

---
 plugins/ltac/pltac.ml  | 2 --
 plugins/ltac/pltac.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 94e398fe5d..052d485bbf 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -46,8 +46,6 @@ let binder_tactic = Entry.create "binder_tactic"
 let tactic = Entry.create "tactic"
 
 (* Main entry for quotations *)
-let tactic_eoi = eoi_entry tactic
-
 let () =
   let open Stdarg in
   let open Tacarg in
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 3a4a081c93..850895c257 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -39,4 +39,3 @@ val tactic_expr : raw_tactic_expr Entry.t
   [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
 val binder_tactic : raw_tactic_expr Entry.t
 val tactic : raw_tactic_expr Entry.t
-val tactic_eoi : raw_tactic_expr Entry.t
-- 
cgit v1.2.3