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.
---
 plugins/ltac/tacentries.ml  | 6 +++---
 plugins/ltac/tacentries.mli | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 0f88734caf..1b212334ce 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -700,7 +700,7 @@ type ('b, 'c) argument_interp =
   (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
-  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_parsing : 'a Vernacextend.argument_rule;
   arg_tag : 'c Val.tag option;
   arg_intern : ('a, 'b) argument_intern;
   arg_subst : 'b argument_subst;
@@ -751,10 +751,10 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
   in
   let () = register_interp0 wit (interp_fun name arg tag) in
   let entry = match arg.arg_parsing with
-  | Vernacentries.Arg_alias e ->
+  | Vernacextend.Arg_alias e ->
     let () = Pcoq.register_grammar wit e in
     e
-  | Vernacentries.Arg_rules rules ->
+  | Vernacextend.Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
     let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
     e
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index c93d6251e0..79f9e093fb 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -128,7 +128,7 @@ type ('b, 'c) argument_interp =
   (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
-  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_parsing : 'a Vernacextend.argument_rule;
   arg_tag : 'c Geninterp.Val.tag option;
   arg_intern : ('a, 'b) argument_intern;
   arg_subst : 'b argument_subst;
-- 
cgit v1.2.3