diff options
| author | herbelin | 2003-11-05 11:51:31 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-05 11:51:31 +0000 |
| commit | d609fcd6ebb1289b04861c94e22c655c48aebf97 (patch) | |
| tree | d62ce5a59629dfe738a0579db87f8e155d45c0a0 | |
| parent | 8588dadbe1e9ea9ebba85bf938ddd93455830f45 (diff) | |
Branchement de Show Script sur l'afficheur structure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4798 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 999b7b9722..d4b6b552e2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -92,7 +92,7 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (Refiner.print_script true evc (Global.named_context()) pf) + msgnl (Refiner.print_treescript true evc (Global.named_context()) pf) let show_top_evars () = let pfts = get_pftreestate () in @@ -983,9 +983,11 @@ let apply_subproof f occ = let pf = proof_of_pftreestate pts in f evc (Global.named_context()) pf -let explain_proof occ = msg (apply_subproof (Refiner.print_script true) occ) +let explain_proof occ = + msg (apply_subproof (Refiner.print_treescript true) occ) -let explain_tree occ = msg (apply_subproof Refiner.print_proof occ) +let explain_tree occ = + msg (apply_subproof Refiner.print_proof occ) let vernac_show = function | ShowGoal nopt -> |