aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacentries.mli')
-rw-r--r--vernac/vernacentries.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 02a3b2bd6..79f9b602a 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