From 998e523743e059783cf587b8ecb12cc909566b02 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 17 Jul 2008 17:50:54 +0000 Subject: 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 --- toplevel/vernacentries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel') 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) -- cgit v1.2.3