aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacentries.mli')
-rw-r--r--vernac/vernacentries.mli2
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