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

7 files changed, 273 insertions, 292 deletions

diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 30fae756e9..ce93a8baaf 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -8,7 +8,7 @@ Himsg
 ExplainErr
 Locality
 Egramml
-Vernacinterp
+Vernacextend
 Ppvernac
 Proof_using
 Lemmas
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 74423d482e..1fab35b650 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -30,7 +30,6 @@ open Constrexpr
 open Redexpr
 open Lemmas
 open Locality
-open Vernacinterp
 open Attributes
 
 module NamedDecl = Context.Named.Declaration
@@ -2268,7 +2267,7 @@ let interp ?proof ~atts ~st c =
   (* Extensions *)
   | VernacExtend (opn,args) ->
     (* XXX: Here we are returning the state! :) *)
-    let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
+    let _st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
     ()
 
 (** A global default timeout, controlled by option "Set Default Timeout n".
@@ -2400,147 +2399,3 @@ let interp ?verbosely ?proof ~st cmd =
     let exn = CErrors.push exn in
     Vernacstate.invalidate_cache ();
     iraise exn
-
-(** VERNAC EXTEND registering *)
-
-open Genarg
-open Extend
-
-type classifier = Genarg.raw_generic_argument list -> vernac_classification
-
-type (_, _) ty_sig =
-| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
-| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
-| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
-
-type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
-
-let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
-
-let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
-| TyNil -> fun f args ->
-  begin match args with
-  | [] -> f
-  | _ :: _ -> type_error ()
-  end
-| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
-| TyNonTerminal (tu, ty) -> fun f args ->
-  begin match args with
-  | [] -> type_error ()
-  | Genarg.GenArg (Rawwit tag, v) :: args ->
-    match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
-    | None -> type_error ()
-    | Some Refl -> untype_classifier ty (f v) args
-  end
-
-(** Stupid GADTs forces us to duplicate the definition just for typing *)
-let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
-| TyNil -> fun f args ->
-  begin match args with
-  | [] -> f
-  | _ :: _ -> type_error ()
-  end
-| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
-| TyNonTerminal (tu, ty) -> fun f args ->
-  begin match args with
-  | [] -> type_error ()
-  | Genarg.GenArg (Rawwit tag, v) :: args ->
-    match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
-    | None -> type_error ()
-    | Some Refl -> untype_command ty (f v) args
-  end
-
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function
-| TUlist1 l -> Alist1 (untype_user_symbol l)
-| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
-| TUlist0 l -> Alist0 (untype_user_symbol l)
-| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
-| TUopt o -> Aopt (untype_user_symbol o)
-| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a))
-| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i)
-
-let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
-| TyNil -> []
-| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
-| TyNonTerminal (tu, ty) ->
-  let t = rawwit (Egramml.proj_symbol tu) in
-  let symb = untype_user_symbol tu in
-  Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
-
-let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
-
-let classifiers : classifier array String.Map.t ref = ref String.Map.empty
-
-let get_vernac_classifier (name, i) args =
-  (String.Map.find name !classifiers).(i) args
-
-let declare_vernac_classifier name f =
-  classifiers := String.Map.add name f !classifiers
-
-let vernac_extend ~command ?classifier ?entry ext =
-  let get_classifier (TyML (_, ty, _, cl)) = match cl with
-  | Some cl -> untype_classifier ty cl
-  | None ->
-    match classifier with
-    | Some cl -> fun _ -> cl command
-    | None ->
-      let e = match entry with
-      | None -> "COMMAND"
-      | Some e -> Pcoq.Gram.Entry.name e
-      in
-      let msg = Printf.sprintf "\
-        Vernac entry \"%s\" misses a classifier. \
-        A classifier is a function that returns an expression \
-        of type vernac_classification (see Vernacexpr). You can: \n\
-        - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \
-          new vernacular command does not alter the system state;\n\
-        - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \
-          new vernacular command alters the system state but not the \
-          parser nor it starts a proof or ends one;\n\
-        - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \
-          a global function f.  The function f will be called passing\
-          \"%s\" as the only argument;\n\
-        - Add a specific classifier in each clause using the syntax:\n\
-          '[...] => [ f ] -> [...]'.\n\
-        Specific classifiers have precedence over global \
-        classifiers. Only one classifier is called."
-          command e e e command
-      in
-      CErrors.user_err (Pp.strbrk msg)
-  in
-  let cl = Array.map_of_list get_classifier ext in
-  let iter i (TyML (depr, ty, f, _)) =
-    let f = untype_command ty f in
-    let r = untype_grammar ty in
-    let () = vinterp_add depr (command, i) f in
-    Egramml.extend_vernac_command_grammar (command, i) entry r
-  in
-  let () = declare_vernac_classifier command cl in
-  List.iteri iter ext
-
-(** VERNAC ARGUMENT EXTEND registering *)
-
-type 'a argument_rule =
-| Arg_alias of 'a Pcoq.Entry.t
-| Arg_rules of 'a Extend.production_rule list
-
-type 'a vernac_argument = {
-  arg_printer : 'a -> Pp.t;
-  arg_parsing : 'a argument_rule;
-}
-
-let vernac_argument_extend ~name arg =
-  let wit = Genarg.create_arg name in
-  let entry = match arg.arg_parsing with
-  | Arg_alias e ->
-    let () = Pcoq.register_grammar wit e in
-    e
-  | 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
-  in
-  let pr = arg.arg_printer in
-  let pr x = Genprint.PrinterBasic (fun () -> pr x) in
-  let () = Genprint.register_vernac_print0 wit pr in
-  (wit, entry)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 8ccd121b8f..8d8d7cfcf0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -36,50 +36,3 @@ val command_focus : unit Proof.focus_kind
 
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
-
-(** {5 VERNAC EXTEND} *)
-
-type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
-
-type (_, _) ty_sig =
-| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
-| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
-| TyNonTerminal :
-  ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
-    ('a -> 'r, 'a -> 's) ty_sig
-
-type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
-
-(** Wrapper to dynamically extend vernacular commands. *)
-val vernac_extend :
-  command:string ->
-  ?classifier:(string -> Vernacexpr.vernac_classification) ->
-  ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
-  ty_ml list -> unit
-
-(** {5 VERNAC ARGUMENT EXTEND} *)
-
-type 'a argument_rule =
-| Arg_alias of 'a Pcoq.Entry.t
-  (** This is used because CAMLP5 parser can be dumb about rule factorization,
-      which sometimes requires two entries to be the same. *)
-| Arg_rules of 'a Extend.production_rule list
-  (** There is a discrepancy here as we use directly extension rules and thus
-    entries instead of ty_user_symbol and thus arguments as roots. *)
-
-type 'a vernac_argument = {
-  arg_printer : 'a -> Pp.t;
-  arg_parsing : 'a argument_rule;
-}
-
-val vernac_argument_extend : name:string -> 'a vernac_argument ->
-  ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
-
-(** {5 STM classifiers} *)
-
-val get_vernac_classifier :
-  Vernacexpr.extend_name -> classifier
-
-(** Low-level API, not for casual user. *)
-val declare_vernac_classifier :
-  string -> classifier array -> unit
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
new file mode 100644
index 0000000000..5fba586298
--- /dev/null
+++ b/vernac/vernacextend.ml
@@ -0,0 +1,211 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+
+type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+
+type plugin_args = Genarg.raw_generic_argument list
+
+(* Table of vernac entries *)
+let vernac_tab =
+  (Hashtbl.create 211 :
+    (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t)
+
+let vinterp_add depr s f =
+  try
+    Hashtbl.add vernac_tab s (depr, f)
+  with Failure _ ->
+    user_err ~hdr:"vinterp_add"
+      (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
+
+let vinterp_map s =
+  try
+    Hashtbl.find vernac_tab s
+  with Failure _ | Not_found ->
+    user_err ~hdr:"Vernac Interpreter"
+      (str"Cannot find vernac command " ++ str (fst s) ++ str".")
+
+let warn_deprecated_command =
+  let open CWarnings in
+  create ~name:"deprecated-command" ~category:"deprecated"
+         (fun pr -> str "Deprecated vernacular command: " ++ pr)
+
+(* Interpretation of a vernac command *)
+
+let call opn converted_args ~atts ~st =
+  let phase = ref "Looking up command" in
+  try
+    let depr, callback = vinterp_map opn in
+    let () = if depr then
+      let rules = Egramml.get_extend_vernac_rule opn in
+      let pr_gram = function
+      | Egramml.GramTerminal s -> str s
+      | Egramml.GramNonTerminal _ -> str "_"
+      in
+      let pr = pr_sequence pr_gram rules in
+      warn_deprecated_command pr;
+    in
+    phase := "Checking arguments";
+    let hunk = callback converted_args in
+    phase := "Executing command";
+    hunk ~atts ~st
+  with
+    | reraise ->
+        let reraise = CErrors.push reraise in
+        if !Flags.debug then
+          Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
+        iraise reraise
+
+(** VERNAC EXTEND registering *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
+
+let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
+| TyNil -> fun f args ->
+  begin match args with
+  | [] -> f
+  | _ :: _ -> type_error ()
+  end
+| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
+| TyNonTerminal (tu, ty) -> fun f args ->
+  let open Genarg in
+  begin match args with
+  | [] -> type_error ()
+  | GenArg (Rawwit tag, v) :: args ->
+    match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+    | None -> type_error ()
+    | Some Refl -> untype_classifier ty (f v) args
+  end
+
+(** Stupid GADTs forces us to duplicate the definition just for typing *)
+let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
+| TyNil -> fun f args ->
+  begin match args with
+  | [] -> f
+  | _ :: _ -> type_error ()
+  end
+| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
+| TyNonTerminal (tu, ty) -> fun f args ->
+  let open Genarg in
+  begin match args with
+  | [] -> type_error ()
+  | GenArg (Rawwit tag, v) :: args ->
+    match genarg_type_eq tag (Egramml.proj_symbol tu) with
+    | None -> type_error ()
+    | Some Refl -> untype_command ty (f v) args
+  end
+
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol =
+  let open Extend in function
+| TUlist1 l -> Alist1 (untype_user_symbol l)
+| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUlist0 l -> Alist0 (untype_user_symbol l)
+| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUopt o -> Aopt (untype_user_symbol o)
+| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a))
+| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i)
+
+let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function
+| TyNil -> []
+| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
+| TyNonTerminal (tu, ty) ->
+  let t = Genarg.rawwit (Egramml.proj_symbol tu) in
+  let symb = untype_user_symbol tu in
+  Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
+
+let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
+
+let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+
+let get_vernac_classifier (name, i) args =
+  (String.Map.find name !classifiers).(i) args
+
+let declare_vernac_classifier name f =
+  classifiers := String.Map.add name f !classifiers
+
+let vernac_extend ~command ?classifier ?entry ext =
+  let get_classifier (TyML (_, ty, _, cl)) = match cl with
+  | Some cl -> untype_classifier ty cl
+  | None ->
+    match classifier with
+    | Some cl -> fun _ -> cl command
+    | None ->
+      let e = match entry with
+      | None -> "COMMAND"
+      | Some e -> Pcoq.Gram.Entry.name e
+      in
+      let msg = Printf.sprintf "\
+        Vernac entry \"%s\" misses a classifier. \
+        A classifier is a function that returns an expression \
+        of type vernac_classification (see Vernacexpr). You can: \n\
+        - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \
+          new vernacular command does not alter the system state;\n\
+        - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \
+          new vernacular command alters the system state but not the \
+          parser nor it starts a proof or ends one;\n\
+        - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \
+          a global function f.  The function f will be called passing\
+          \"%s\" as the only argument;\n\
+        - Add a specific classifier in each clause using the syntax:\n\
+          '[...] => [ f ] -> [...]'.\n\
+        Specific classifiers have precedence over global \
+        classifiers. Only one classifier is called."
+          command e e e command
+      in
+      CErrors.user_err (Pp.strbrk msg)
+  in
+  let cl = Array.map_of_list get_classifier ext in
+  let iter i (TyML (depr, ty, f, _)) =
+    let f = untype_command ty f in
+    let r = untype_grammar ty in
+    let () = vinterp_add depr (command, i) f in
+    Egramml.extend_vernac_command_grammar (command, i) entry r
+  in
+  let () = declare_vernac_classifier command cl in
+  List.iteri iter ext
+
+(** VERNAC ARGUMENT EXTEND registering *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+| Arg_rules of 'a Extend.production_rule list
+
+type 'a vernac_argument = {
+  arg_printer : 'a -> Pp.t;
+  arg_parsing : 'a argument_rule;
+}
+
+let vernac_argument_extend ~name arg =
+  let wit = Genarg.create_arg name in
+  let entry = match arg.arg_parsing with
+  | Arg_alias e ->
+    let () = Pcoq.register_grammar wit e in
+    e
+  | 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
+  in
+  let pr = arg.arg_printer in
+  let pr x = Genprint.PrinterBasic (fun () -> pr x) in
+  let () = Genprint.register_vernac_print0 wit pr in
+  (wit, entry)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
new file mode 100644
index 0000000000..bb94f3a6a9
--- /dev/null
+++ b/vernac/vernacextend.mli
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Interpretation of extended vernac phrases. *)
+
+type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+
+type plugin_args = Genarg.raw_generic_argument list
+
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+
+(** {5 VERNAC EXTEND} *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+  ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
+    ('a -> 'r, 'a -> 's) ty_sig
+
+type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+(** Wrapper to dynamically extend vernacular commands. *)
+val vernac_extend :
+  command:string ->
+  ?classifier:(string -> Vernacexpr.vernac_classification) ->
+  ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
+  ty_ml list -> unit
+
+(** {5 VERNAC ARGUMENT EXTEND} *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+  (** This is used because CAMLP5 parser can be dumb about rule factorization,
+      which sometimes requires two entries to be the same. *)
+| Arg_rules of 'a Extend.production_rule list
+  (** There is a discrepancy here as we use directly extension rules and thus
+    entries instead of ty_user_symbol and thus arguments as roots. *)
+
+type 'a vernac_argument = {
+  arg_printer : 'a -> Pp.t;
+  arg_parsing : 'a argument_rule;
+}
+
+val vernac_argument_extend : name:string -> 'a vernac_argument ->
+  ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
+
+(** {5 STM classifiers} *)
+
+val get_vernac_classifier :
+  Vernacexpr.extend_name -> classifier
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
deleted file mode 100644
index eb4282705e..0000000000
--- a/vernac/vernacinterp.ml
+++ /dev/null
@@ -1,77 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Pp
-open CErrors
-
-type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
-
-type plugin_args = Genarg.raw_generic_argument list
-
-(* Table of vernac entries *)
-let vernac_tab =
-  (Hashtbl.create 211 :
-    (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t)
-
-let vinterp_add depr s f =
-  try
-    Hashtbl.add vernac_tab s (depr, f)
-  with Failure _ ->
-    user_err ~hdr:"vinterp_add"
-      (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
-
-let overwriting_vinterp_add s f =
-  begin
-    try
-      let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s
-    with Not_found -> ()
-  end;
-  Hashtbl.add vernac_tab s (false, f)
-
-let vinterp_map s =
-  try
-    Hashtbl.find vernac_tab s
-  with Failure _ | Not_found ->
-    user_err ~hdr:"Vernac Interpreter"
-      (str"Cannot find vernac command " ++ str (fst s) ++ str".")
-
-let vinterp_init () = Hashtbl.clear vernac_tab
-
-let warn_deprecated_command =
-  let open CWarnings in
-  create ~name:"deprecated-command" ~category:"deprecated"
-         (fun pr -> str "Deprecated vernacular command: " ++ pr)
-
-(* Interpretation of a vernac command *)
-
-let call opn converted_args ~atts ~st =
-  let phase = ref "Looking up command" in
-  try
-    let depr, callback = vinterp_map opn in
-    let () = if depr then
-      let rules = Egramml.get_extend_vernac_rule opn in
-      let pr_gram = function
-      | Egramml.GramTerminal s -> str s
-      | Egramml.GramNonTerminal _ -> str "_"
-      in
-      let pr = pr_sequence pr_gram rules in
-      warn_deprecated_command pr;
-    in
-    phase := "Checking arguments";
-    let hunk = callback converted_args in
-    phase := "Executing command";
-    hunk ~atts ~st
-  with
-    | reraise ->
-        let reraise = CErrors.push reraise in
-        if !Flags.debug then
-	  Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
-        iraise reraise
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
deleted file mode 100644
index 0fc02c6915..0000000000
--- a/vernac/vernacinterp.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Interpretation of extended vernac phrases. *)
-
-type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
-
-type plugin_args = Genarg.raw_generic_argument list
-
-val vinterp_init : unit -> unit
-val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
-val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
-
-val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t