ntrefiner.ml* removed in module xml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 6 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 6364d258c3..ee1bf8775d 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -543,16 +543,17 @@ let print id fn =
 (*  where dest is either None (for stdout) or (Some filename) *)
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 let show fn =
-(*
  let pftst = Pfedit.get_pftreestate () in
- let id = Pfedit.get_proof () in
+ let id = Pfedit.get_current_proof_name () in
  let pf = Tacmach.proof_of_pftreestate pftst in
- let typ = (Proof_trees.goal_of_proof pf).Evd.concl in
+ let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in
+(*V7
  (*CSC: ntrefiner copied verbatim from natural, used, but _not_ understood *)
  let val0, mv = Ntrefiner.nt_extract_open_proof (Vartab.initial_sign ()) pf in
- let mv_t = List.map (function i, (t, _) -> i,t) mv in
-  Xml.pp (print_current_proof val0 typ id mv_t) fn
-*) ()
+*)
+ let val0,mv = Tacmach.extract_open_pftreestate pftst in
+ (*let mv_t = List.map (function i, (t, _) -> i,t) mv in*)
+  Xml.pp (print_current_proof val0 typ (Names.string_of_id id) mv) fn
 ;;
 
 (* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *)