aboutsummaryrefslogtreecommitdiff
path: root/vernac/attributes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/attributes.ml')
-rw-r--r--vernac/attributes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index bc0b0310b3..75ca027332 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -162,7 +162,7 @@ let universe_transform ~warn_unqualified : unit attribute =
let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
let is_universe_polymorphism =
let b = ref false in
- let _ = let open Goptions in
+ let () = let open Goptions in
declare_bool_option
{ optdepr = false;
optname = "universe polymorphism";