Remove dead code that used to be there for CamlpX compatibility.

Part of this code has been introduced very recently in 7c62654 in spite of
the existence of a proper API. This means that this should be better
documented.

2 files changed, 4 insertions, 76 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 997ea78e6..93d65df2f 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -86,11 +86,6 @@ module type S =
   type internal_entry = Tok.t Gramext.g_entry
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statement =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statement =
-      Gramext.position option * single_extend_statement list
   type coq_parsable
 
   val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
@@ -101,9 +96,6 @@ module type S =
 
   val comment_state : coq_parsable -> ((int * int) * string) list
 
-  val srules' : production_rule list -> symbol
-  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
-
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
   include Grammar.GMake(CLexer)
@@ -112,11 +104,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   type internal_entry = Tok.t Gramext.g_entry
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statement =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statement =
-      Gramext.position option * single_extend_statement list
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
@@ -147,10 +134,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
   let entry_print ft x = Entry.print ft x
 
-  (* Not used *)
-  let srules' = Gramext.srules
-  let parse_tokens_after_filter = Entry.parse_token
-
 end
 
 let warning_verbose = Gramext.warning_verbose
@@ -246,7 +229,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aentryl (e, n) ->
     Symbols.snterml (G.Entry.obj e, n)
   | Arules rs ->
-    G.srules' (List.map symbol_of_rules rs)
+    Gramext.srules (List.map symbol_of_rules rs)
 
 and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
 | Stop -> fun accu -> accu
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 154de1221..ae4f5cab6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -16,63 +16,18 @@ open Libnames
 
 (** The parser of Coq *)
 
+(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE.
+    We only have it here to work with Camlp5. Handwritten grammar extensions
+    should use the safe [Pcoq.grammar_extend] function below. *)
 module Gram : sig
 
   include Grammar.S with type te = Tok.t
 
-(* Where Grammar.S is
-
-module type S =
-  sig
-    type te = 'x;
-    type parsable = 'x;
-    value parsable : Stream.t char -> parsable;
-    value tokens : string -> list (string * int);
-    value glexer : Plexing.lexer te;
-    value set_algorithm : parse_algorithm -> unit;
-    module Entry :
-      sig
-        type e 'a = 'y;
-        value create : string -> e 'a;
-        value parse : e 'a -> parsable -> 'a;
-        value parse_token : e 'a -> Stream.t te -> 'a;
-        value name : e 'a -> string;
-        value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
-        value print : Format.formatter -> e 'a -> unit;
-        external obj : e 'a -> Gramext.g_entry te = "%identity";
-      end
-    ;
-    module Unsafe :
-      sig
-        value gram_reinit : Plexing.lexer te -> unit;
-        value clear_entry : Entry.e 'a -> unit;
-      end
-    ;
-    value extend :
-      Entry.e 'a -> option Gramext.position ->
-        list
-          (option string * option Gramext.g_assoc *
-           list (list (Gramext.g_symbol te) * Gramext.g_action)) ->
-        unit;
-    value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit;
-  end
-
-*)
-
   type 'a entry = 'a Entry.e
-  type internal_entry = Tok.t Gramext.g_entry
-  type symbol = Tok.t Gramext.g_symbol
-  type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statement =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statement =
-      Gramext.position option * single_extend_statement list
 
   type coq_parsable
 
   val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
-  val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
@@ -82,18 +37,8 @@ module type S =
 
   val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit
 
-  (* Apparently not used *)
-  val srules' : production_rule list -> symbol
-  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
-
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
-module Symbols : sig
-
-  val stoken : Tok.t -> Gram.symbol
-  val snterm : Gram.internal_entry -> Gram.symbol
-end
-
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using