aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/mod_checking.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3c9e1cac5..63e28448f 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -25,7 +25,7 @@ let refresh_arity ar =
| _ -> ar, Univ.ContextSet.empty
let check_constant_declaration env kn cb =
- Feedback.msg_notice (str " checking cst:" ++ prcon kn);
+ Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn);
(** [env'] contains De Bruijn universe variables *)
let env' =
match cb.const_universes with