Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.

Renaming it register_grammars_by_name.

5 files changed, 22 insertions, 15 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 54e7949ae..ddb26d771 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -638,3 +638,15 @@ let () =
   Grammar.register0 wit_constr (Constr.constr);
   Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
+
+(** Registering extra grammar *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammars_by_name name grams =
+  grammar_names := String.Map.add name grams !grammar_names
+
+let find_grammars_by_name name =
+  String.Map.find name !grammar_names
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 75378d2c6..accb51366 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -315,3 +315,10 @@ val (!@) : Ploc.t -> Loc.t
 
 type frozen_t
 val parser_summary_tag : frozen_t Summary.Dyn.tag
+
+(** Registering grammars by name *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+val register_grammars_by_name : string -> any_entry list -> unit
+val find_grammars_by_name : string -> any_entry list
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ee84be541..8112cc400 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -545,11 +545,10 @@ let print_located_tactic qid =
 (** Grammar *)
 
 let () =
-  let open Metasyntax in
   let entries = [
     AnyEntry Pltac.tactic_expr;
     AnyEntry Pltac.binder_tactic;
     AnyEntry Pltac.simple_tactic;
     AnyEntry Pltac.tactic_arg;
   ] in
-  register_grammar "tactic" entries
+  register_grammars_by_name "tactic" entries
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index a1c8902c5..da8dda9c2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -43,13 +43,6 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 let entry_buf = Buffer.create 64
 
-type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
-
-let grammars : any_entry list String.Map.t ref = ref String.Map.empty
-
-let register_grammar name grams =
-  grammars := String.Map.add name grams !grammars
-
 let pr_entry e =
   let () = Buffer.clear entry_buf in
   let ft = Format.formatter_of_buffer entry_buf in
@@ -57,11 +50,11 @@ let pr_entry e =
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
-  let gram = try Some (String.Map.find name !grammars) with Not_found -> None in
+  let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in
   match gram with
   | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
   | Some entries ->
-    let pr_one (AnyEntry e) =
+    let pr_one (Pcoq.AnyEntry e) =
       str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++
       pr_entry e
     in
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index e064b570e..9137f7a7e 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -55,10 +55,6 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
 
 val pr_grammar : string -> Pp.t
 
-type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
-
-val register_grammar : string -> any_entry list -> unit
-
 val check_infix_modifiers : syntax_modifier list -> unit
 
 val with_syntax_protection : ('a -> 'b) -> 'a -> 'b