From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 vernac/vernacentries.mli | 40 ++++++++++++++++++++++++++++++++++++----
 1 file changed, 36 insertions(+), 4 deletions(-)

(limited to 'vernac/vernacentries.mli')

diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f6199e82..fb2a30ba 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,13 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
-
-val dump_global : Libnames.reference or_by_notation -> unit
+val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
 
 (** Vernacular entries *)
 val vernac_require :
-  Libnames.reference option -> bool option -> Libnames.reference list -> unit
+  Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
 
 (** The main interpretation function of vernacular expressions *)
 val interp :
@@ -40,3 +38,37 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
 val universe_polymorphism_option_name : string list
+
+(** Elaborate a [atts] record out of a list of flags.
+    Also returns whether polymorphism is explicitly (un)set. *)
+val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+
+(** {5 VERNAC EXTEND} *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+type (_, _) ty_sig =
+| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
+| TyNonTerminal :
+  string option *
+  ('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 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
-- 
cgit v1.2.3