diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-25 09:35:25 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:06:00 +0000 |
| commit | 4371ff2357c11d913b163dde193255f538f3565f (patch) | |
| tree | 8ea3560c5d1010729cb1f51e01eabc36a22ce36d /vernac/vernacentries.mli | |
| parent | 3c83ca8b3ea9ec3ea6656dc7f726c46a21729541 (diff) | |
[vernac] Generic syntax for flags/attributes
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 79f9b602a..79f9c05ad 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -41,4 +41,4 @@ 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_flag list -> Vernacinterp.atts -> bool option * Vernacinterp.atts +val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts |