diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-07-09 22:16:10 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-07-09 22:16:10 +0200 |
| commit | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (patch) | |
| tree | 7f16c4018bad54d9c1bf7c9e9d4aefacd83b2e40 /vernac/vernacentries.mli | |
| parent | c1d4dc68ace54f9ff9fd8f6466add38098ef0495 (diff) | |
| parent | 420b38cba7aedfcfeac5671a7db0c02c4bb14a0c (diff) | |
Merge PR #7920: Generic syntax for attributes
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 02a3b2bd6..79f9c05ad 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_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts |