aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_using.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_using.ml')
-rw-r--r--proofs/proof_using.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f51586c73..2c489d6de 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids =
let suggest_Proof_using name env vars ids_typ context_ids =
let module S = Id.Set in
let open Pp in
- let print x = Feedback.msg_error x in
+ let print x = Feedback.msg_debug x in
let pr_set parens s =
let wrap ppcmds =
if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"