aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.ml')
-rw-r--r--proofs/proofview.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bf4a1e5a69..d55689a202 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -967,7 +967,9 @@ module Trace = struct
let log m = InfoL.leaf (Info.Msg m)
let name_tactic m t = InfoL.tag (Info.Tactic m) t
- let pr_info = Info.print
+ let pr_info ?(lvl=0) info =
+ assert (lvl >= 0);
+ Info.(print (collapse lvl info))
end