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 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/ltac/pltac.ml')

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
-- 
cgit v1.2.3