diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2017-12-11 17:02:55 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2017-12-29 14:12:45 +0000 |
| commit | 557f017f2decd056cb04a6b87719a9d82c80a425 (patch) | |
| tree | c7a65fb09d15fa6d9280ff0e5f5150c7e6790f9e /vernac/vernacinterp.ml | |
| parent | 4cdb838ef260c12f59cb91915c78dc975bd4c157 (diff) | |
[vernac] adds the “program” flag to the “atts” record
Diffstat (limited to 'vernac/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index c0b93c163..c40ca27db 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -16,6 +16,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 |