Merge PR #7898: Remove camlp4 remains

9 files changed, 42 insertions, 43 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 48f225f97..3281b75aa 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -240,14 +240,14 @@ type (_, _) entry =
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
 (* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option =
+let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
   fun forpat level -> match forpat with
   | ForConstr ->
     if level = 200 then Constr.binder_constr, None
     else Constr.operconstr, Some level
   | ForPattern -> Constr.pattern, Some level
 
-let target_entry : type s. s target -> s Gram.entry = function
+let target_entry : type s. s target -> s Entry.t = function
 | ForConstr -> Constr.operconstr
 | ForPattern -> Constr.pattern
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 31aa1a989..a5ee036db 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -21,7 +21,7 @@ type 's grammar_prod_item =
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+  Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option ->
     vernac_expr grammar_prod_item list -> unit
 
 val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index cccdbfc91..dacef6e21 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -22,7 +22,7 @@ open Pvernac.Vernac_
 
 let thm_token = G_vernac.thm_token
 
-let hint = Gram.entry_create "hint"
+let hint = Entry.create "hint"
 
 let warn_deprecated_focus =
   CWarnings.create ~name:"deprecated-focus" ~category:"deprecated"
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e9d6ed9f6..a35a1998d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -37,18 +37,18 @@ let _ = List.iter CLexer.add_keyword vernac_kw
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
-let query_command = Gram.entry_create "vernac:query_command"
-
-let subprf = Gram.entry_create "vernac:subprf"
-
-let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
-let thm_token = Gram.entry_create "vernac:thm_token"
-let def_body = Gram.entry_create "vernac:def_body"
-let decl_notation = Gram.entry_create "vernac:decl_notation"
-let record_field = Gram.entry_create "vernac:record_field"
-let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
-let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
+let query_command = Entry.create "vernac:query_command"
+
+let subprf = Entry.create "vernac:subprf"
+
+let class_rawexpr = Entry.create "vernac:class_rawexpr"
+let thm_token = Entry.create "vernac:thm_token"
+let def_body = Entry.create "vernac:def_body"
+let decl_notation = Entry.create "vernac:decl_notation"
+let record_field = Entry.create "vernac:record_field"
+let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
+let instance_name = Entry.create "vernac:instance_name"
+let section_subset_expr = Entry.create "vernac:section_subset_expr"
 
 let make_bullet s =
   let open Proof_bullet in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 240147c8d..33e6229b2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -49,7 +49,7 @@ let entry_buf = Buffer.create 64
 let pr_entry e =
   let () = Buffer.clear entry_buf in
   let ft = Format.formatter_of_buffer entry_buf in
-  let () = Pcoq.Gram.entry_print ft e in
+  let () = Pcoq.Entry.print ft e in
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index f8b085f3e..74e53bef1 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -178,7 +178,7 @@ let suggest_variable env id =
 let value = ref None
 
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
-let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us)))
+let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
 let _ =
   Goptions.declare_stringopt_option
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index bac882381..b2fa8ec99 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -10,13 +10,11 @@
 
 open Pcoq
 
-let uncurry f (x,y) = f x y
-
 let uvernac = create_universe "vernac"
 
 module Vernac_ =
   struct
-    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+    let gec_vernac s = Entry.create ("vernac:" ^ s)
 
     (* The different kinds of vernacular commands *)
     let gallina = gec_vernac "gallina"
@@ -28,22 +26,23 @@ module Vernac_ =
     let red_expr = new_entry utactic "red_expr"
     let hint_info = gec_vernac "hint_info"
     (* Main vernac entry *)
-    let main_entry = Gram.entry_create "vernac"
+    let main_entry = Entry.create "vernac"
     let noedit_mode = gec_vernac "noedit_command"
 
     let () =
-      let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
-      let act_eoi = Gram.action (fun _ loc -> None) in
+      let open Extend in
+      let act_vernac v loc = Some (loc, v) in
+      let act_eoi _ loc = None in
       let rule = [
-        ([ Symbols.stoken Tok.EOI ], act_eoi);
-        ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
+        Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
+        Rule (Next (Stop, Aentry vernac_control), act_vernac);
       ] in
-      uncurry (Gram.extend main_entry) (None, [None, None, rule])
+      Pcoq.grammar_extend main_entry None (None, [None, None, rule])
 
     let command_entry_ref = ref noedit_mode
     let command_entry =
       Gram.Entry.of_parser "command_entry"
-        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+        (fun strm -> Gram.Entry.parse_token !command_entry_ref strm)
 
   end
 
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 2993a1661..b2f8f7146 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -16,21 +16,21 @@ val uvernac : gram_universe
 
 module Vernac_ :
   sig
-    val gallina : vernac_expr Gram.entry
-    val gallina_ext : vernac_expr Gram.entry
-    val command : vernac_expr Gram.entry
-    val syntax : vernac_expr Gram.entry
-    val vernac_control : vernac_control Gram.entry
-    val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val noedit_mode : vernac_expr Gram.entry
-    val command_entry : vernac_expr Gram.entry
-    val red_expr : raw_red_expr Gram.entry
-    val hint_info : Hints.hint_info_expr Gram.entry
+    val gallina : vernac_expr Entry.t
+    val gallina_ext : vernac_expr Entry.t
+    val command : vernac_expr Entry.t
+    val syntax : vernac_expr Entry.t
+    val vernac_control : vernac_control Entry.t
+    val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
+    val noedit_mode : vernac_expr Entry.t
+    val command_entry : vernac_expr Entry.t
+    val red_expr : raw_red_expr Entry.t
+    val hint_info : Hints.hint_info_expr Entry.t
   end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Entry.t
 
 (** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Gram.entry
-val set_command_entry : vernac_expr Gram.entry -> unit
+val get_command_entry : unit -> vernac_expr Entry.t
+val set_command_entry : vernac_expr Entry.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 27f2a740e..b6bc76a2e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2040,7 +2040,7 @@ let vernac_load interp fname =
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Gram.entry_parse Pvernac.main_entry po with
+    match Pcoq.Entry.parse Pvernac.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
@@ -2049,7 +2049,7 @@ let vernac_load interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
+    Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
   begin
     try while true do interp (snd (parse_sentence input)) done
     with End_of_input -> ()