Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move extension functions there

3 files changed, 12 insertions, 13 deletions

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index b882d2164f..715b8cd23f 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -75,9 +75,9 @@ let is_ident x = function
 let make_extend loc self cl = match cl with
 | [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
   (** Special handling of identity arguments by not redeclaring an entry *)
-  <:expr< Vernacentries.Arg_alias $lid:e$ >>
+  <:expr< Vernacextend.Arg_alias $lid:e$ >>
 | _ ->
-  <:expr< Vernacentries.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >>
+  <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >>
 
 let warning_deprecated prefix s = function
 | None -> ()
@@ -144,9 +144,9 @@ let declare_vernac_argument loc s pr cl =
   let pr_rules = match pr with
     | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >>
     | Some pr -> <:expr< $lid:pr$ >> in
-  declare_arg loc s <:expr< Vernacentries.vernac_argument_extend ~{ name = $se$ } {
-    Vernacentries.arg_printer = $pr_rules$;
-    Vernacentries.arg_parsing = $make_extend loc s cl$
+  declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } {
+    Vernacextend.arg_printer = $pr_rules$;
+    Vernacextend.arg_parsing = $make_extend loc s cl$
   } >>
 
 open Pcaml
diff --git a/grammar/dune b/grammar/dune
index f03fe07607..78df2826d6 100644
--- a/grammar/dune
+++ b/grammar/dune
@@ -1,8 +1,7 @@
 (library
- (name grammar)
+ (name grammar5)
  (synopsis "Coq Camlp5 Grammar Extensions for Plugins")
  (public_name coq.grammar)
- (wrapped false)
  (flags (:standard -w -58))
  (libraries camlp5))
 
@@ -14,7 +13,7 @@
 
 (rule
  (targets coqp5)
- (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5)))
+ (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5)))
 
 (install
  (section bin)
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 3c401e827e..d44eeef670 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -25,24 +25,24 @@ type rule = {
 }
 
 let rec mlexpr_of_clause = function
-| [] -> <:expr< Vernacentries.TyNil >>
-| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
+| [] -> <:expr< Vernacextend.TyNil >>
+| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
 | ExtNonTerminal (g, id) :: cl ->
-  <:expr< Vernacentries.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
+  <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 let make_rule r =
   let ty = mlexpr_of_clause r.r_patt in
   let cmd = binders_of_tokens r.r_branch r.r_patt in
   let make_classifier c = binders_of_tokens c r.r_patt in
   let classif = mlexpr_of_option make_classifier r.r_class in
-  <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
+  <:expr< Vernacextend.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
   let c = mlexpr_of_option (fun x -> x) c in
   let rules = mlexpr_of_list make_rule cl in
   declare_str_items loc
-  [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
+  [ <:str_item< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
 
 open Pcaml