From 4aa99307874c59f97570f624a06463aaa8115ec5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Nov 2018 14:25:33 +0100
Subject: [vernac] Rename Vernacinterp to Vernacextend and move extension
 functions there.

This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.

We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.

Note the beneficial effects on reducing the `.mli` API.
---
 grammar/argextend.mlp    | 10 +++++-----
 grammar/dune             |  5 ++---
 grammar/vernacextend.mlp | 10 +++++-----
 3 files changed, 12 insertions(+), 13 deletions(-)

(limited to 'grammar')

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
 
-- 
cgit v1.2.3