aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-03-22 23:23:14 +0100
committerEmilio Jesus Gallego Arias2017-03-24 13:14:59 +0100
commit43ac25fd5218fb92b3971c8df8be4f38894e27f3 (patch)
tree03f1da9560f09a0c04d4c2823ae30b8459988556 /proofs
parent530cd175c1b7465c3fa35c300f42b022bed9b25b (diff)
[nit] Fix a couple incorrect uses of msg_error.
Diffstat (limited to 'proofs')
-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 f51586c739..2c489d6ded 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 ")"