diff options
| author | Vincent Laporte | 2018-02-26 08:54:58 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-07-03 15:54:22 +0000 |
| commit | 9e75cacd86d491f81da7171c72569ac0cb6aeae0 (patch) | |
| tree | 27739fc3dd415876dd842364a92ad7c728c50c92 /vernac/vernacentries.mli | |
| parent | 218c6cebf770a15fb3ca6eca1d587f42b8994234 (diff) | |
[vernac] attribute_of_flags
Elaborate a [atts] record out of a list of flags.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 02a3b2bd61..79f9b602a2 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -38,3 +38,7 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr Evd.evar_map * Redexpr.red_expr) Hook.t 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 |