aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacinterp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacinterp.mli')
-rw-r--r--vernac/vernacinterp.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index ab3d4bfc5..c5e610f89 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -14,6 +14,7 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ program : bool;
}
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t