From 32d47cdb09df5387b28ed9b435456db7630f6b6d Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 26 Oct 2000 09:10:11 +0000
Subject: ntrefiner.ml* removed in module xml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'contrib/xml/xmlcommand.ml')

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 *)
-- 
cgit v1.2.3