aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f5768888c..23f26038e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -95,7 +95,7 @@ let show_script () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- msgnl (print_treescript true evc pf)
+ msgnl_with Pp_control.deep_ft (print_treescript true evc pf)
let show_thesis () =
msgnl (anomaly "TODO" )