Remove the unsafe camlp5 API from the Coq codebase.

3 files changed, 9 insertions, 50 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index e25f7aa54f..b3ae24e941 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -81,7 +81,7 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let lpar_id_coloneq =
-  Gram.Entry.of_parser "test_lpar_id_coloneq"
+  Pcoq.Entry.of_parser "test_lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -96,7 +96,7 @@ let lpar_id_coloneq =
         | _ -> err ())
 
 let impl_ident_head =
-  Gram.Entry.of_parser "impl_ident_head"
+  Pcoq.Entry.of_parser "impl_ident_head"
     (fun strm ->
       match stream_nth 0 strm with
 	| KEYWORD "{" ->
@@ -109,7 +109,7 @@ let impl_ident_head =
 	| _ -> err ())
 
 let name_colon =
-  Gram.Entry.of_parser "name_colon"
+  Pcoq.Entry.of_parser "name_colon"
     (fun strm ->
       match stream_nth 0 strm with
 	| IDENT s ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 01a542b6f3..170df6ad09 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,7 +14,6 @@ open Extend
 open Genarg
 open Gramlib
 
-let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
 
 (** Location Utils  *)
@@ -141,6 +140,9 @@ struct
   let create = G.Entry.create
   let parse = G.entry_parse
   let print = G.Entry.print
+  let of_parser = G.Entry.of_parser
+  let name = G.Entry.name
+  let parse_token_stream = G.Entry.parse_token_stream
 
 end
 
@@ -289,22 +291,6 @@ let grammar_delete e reinit (pos,rls) =
     (G.safe_extend e) (Some ext) [Some lev,Some a,[]]
   | None -> ()
 
-let unsafe_grammar_delete e reinit (pos,rls) =
-  List.iter
-    (fun (n,ass,lev) ->
-      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
-    (List.rev rls);
-  match reinit with
-  | Some (a,ext) ->
-    let a = of_coq_assoc a in
-    let ext = of_coq_position ext in
-    let lev = match pos with
-    | Some (Gramext.Level n) -> n
-    | _ -> assert false
-    in
-    (G.extend e) (Some ext) [Some lev,Some a,[]]
-  | None -> ()
-
 (** Extension *)
 
 let grammar_extend e reinit ext =
@@ -326,25 +312,6 @@ let grammar_extend_sync e reinit ext =
 module Gram =
   struct
     include G
-    let extend e =
-      curry
-    (fun ext ->
-      camlp5_state :=
-        (ByEXTEND ((fun () -> unsafe_grammar_delete e None ext),
-           (fun () -> uncurry (G.extend e) ext)))
-      :: !camlp5_state;
-      uncurry (G.extend e) ext)
-    let delete_rule e pil =
-      (* spiwack: if you use load an ML module which contains GDELETE_RULE
-      in a section, God kills a kitty. As it would corrupt remove_grammars.
-          There does not seem to be a good way to undo a delete rule. As deleting
-      takes fewer arguments than extending. The production rule isn't returned
-      by delete_rule. If we could retrieve the necessary information, then
-      ByEXTEND provides just the framework we need to allow this in section.
-      I'm not entirely sure it makes sense, but at least it would be more correct.
-          *)
-      G.delete_rule e pil
-    let gram_extend e ext = grammar_extend e None ext
   end
 
 (** Remove extensions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 593cf59341..e64c614149 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -17,17 +17,6 @@ open Gramlib
 
 (** 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
-
-  val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit
-
-end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
-
 module Parsable :
 sig
   type t
@@ -41,6 +30,9 @@ module Entry : sig
   val create : string -> 'a t
   val parse : 'a t -> Parsable.t -> 'a
   val print : Format.formatter -> 'a t -> unit
+  val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t
+  val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
+  val name : 'a t -> string
 end
 
 (** The parser of Coq is built from three kinds of rule declarations: