Merge PR #13447: Remove unused parsing code

Reviewed-by: herbelin

1 files changed, 1 insertions, 23 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"