aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-17 17:50:54 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-17 17:50:54 +0000
commit998e523743e059783cf587b8ecb12cc909566b02 (patch)
tree704fd9dd658cb2e7df1e88f0d3115a8d62217e47 /toplevel
parent6d28daee5feee9da501c758cc0516e57660a252e (diff)
fixed indentation of subgoals for Show Script
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11233 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernacentries.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d761472c9..981e82b93 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_with !Pp_control.deep_ft (print_treescript true evc pf)
+ msgnl_with !Pp_control.deep_ft (print_treescript evc pf)
let show_thesis () =
msgnl (anomaly "TODO" )
@@ -1206,7 +1206,7 @@ let apply_subproof f occ =
f evc (Global.named_context()) pf
let explain_proof occ =
- msg (apply_subproof (fun evd _ -> print_treescript true evd) occ)
+ msg (apply_subproof (fun evd _ -> print_treescript evd) occ)
let explain_tree occ =
msg (apply_subproof print_proof occ)