aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 71f7f39a3e..44120dcb3b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1383,7 +1383,7 @@ let vernac_print = function
let st = Conv_oracle.get_transp_state () in
let nassums =
Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
- msg (Printer.pr_assumptionset (Global.env ()) nassums)
+ msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)
let global_module r =
let (loc,qid) = qualid_of_reference r in