aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_using.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-04-04 16:55:56 +0200
committerMaxime Dénès2017-04-04 16:55:56 +0200
commitc112063ba5f562d511ed0cbd754a41539fc48fe1 (patch)
tree1f7e244b3d3b0963d07463604d77bdf35001e67c /proofs/proof_using.ml
parentb824d8ad00001f6c41d0fc8bbf528dccb937c887 (diff)
parentea10a2da9ac11ea57e9eb80d0d6baf9321886da4 (diff)
Merge branch 'trunk' into pr379
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 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 ")"