From 5510629f8b2aa7bd32edc955d6ce0baae8b00f45 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 30 Nov 2020 11:31:57 -0800
Subject: Revert removal of eoi_entry in #13447

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

(limited to 'plugins')

diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 80c13a3698..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -47,6 +47,8 @@ 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 73bce84d18..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -40,3 +40,4 @@ 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