aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacinterp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacinterp.mli')
-rw-r--r--vernac/vernacinterp.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 935cacf77..a24bcd40d 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -19,6 +19,9 @@ type atts = {
program : bool;
}
+val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
+ ?polymorphic: bool -> ?program: bool -> unit -> atts
+
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
type plugin_args = Genarg.raw_generic_argument list