aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/mod_checking.ml')
-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 c07a35e35..7f93e1560 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
| _ -> ar, Univ.ContextSet.empty
let check_constant_declaration env kn cb =
- Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush ();
+ Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn);
let env' =
if cb.const_polymorphic then
let inst = Univ.make_abstract_instance cb.const_universes in