diff options
Diffstat (limited to 'vernac/vernacinterp.mli')
-rw-r--r-- | vernac/vernacinterp.mli | 1 |
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 |