Merge PR #13447: Remove unused parsing code

Reviewed-by: herbelin

4 files changed, 1 insertions, 29 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index d49a49d242..a482e044d8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -175,28 +175,7 @@ let rec remove_grammars n =
            camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries;
            remove_grammars (n - 1)
 
-let make_rule r = [None, None, r]
-
-(** An entry that checks we reached the end of the input. *)
-
-let eoi_entry en =
-  let e = Entry.make ((Entry.name en) ^ "_eoi") in
-  let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (Symbol.token Tok.PEOI) in
-  let act = fun _ x loc -> x in
-  let ext = { pos = None; data = make_rule [Production.make symbs act] } in
-  safe_extend e ext;
-  e
-
-let map_entry f en =
-  let e = Entry.make ((Entry.name en) ^ "_map") in
-  let symbs = Rule.next Rule.stop (Symbol.nterm en) in
-  let act = fun x loc -> f x in
-  let ext = { pos = None; data = make_rule [Production.make symbs act] } in
-  safe_extend e ext;
-  e
-
-(* Parse a string, does NOT check if the entire string was read
-   (use eoi_entry) *)
+(* Parse a string, does NOT check if the entire string was read *)
 
 let parse_string f ?loc x =
   let strm = Stream.of_string x in
@@ -310,7 +289,6 @@ module Constr =
     let constr = Entry.create "constr"
     let term = Entry.create "term"
     let operconstr = term
-    let constr_eoi = eoi_entry constr
     let lconstr = Entry.create "lconstr"
     let binder_constr = Entry.create "binder_constr"
     let ident = Entry.create "ident"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d0ae594db1..df9084ab76 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -120,8 +120,6 @@ end
 (** Parse a string *)
 
 val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
-val eoi_entry : 'a Entry.t -> 'a Entry.t
-val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
 
 type gram_universe [@@deprecated "Deprecated in 8.13"]
 [@@@ocaml.warning "-3"]
@@ -182,7 +180,6 @@ module Prim :
 module Constr :
   sig
     val constr : constr_expr Entry.t
-    val constr_eoi : constr_expr Entry.t
     val lconstr : constr_expr Entry.t
     val binder_constr : constr_expr Entry.t
     val term : constr_expr Entry.t
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 196a68e67c..80c13a3698 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -47,8 +47,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 c0bf6b9f76..73bce84d18 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -40,4 +40,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