ntrefiner.ml* removed in module xml

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

4 files changed, 8 insertions, 91 deletions

diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index c5ee6c836e..01461afbf8 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -8,7 +8,7 @@
 (*                                 17/11/1999                                 *)
 (******************************************************************************)
 
-Declare ML Module "ntrefiner" "xml" "cooking" "xmlcommand" "xmlentries".
+Declare ML Module "xml" "cooking" "xmlcommand" "xmlentries".
 
 Grammar vernac vernac : Ast :=
   xml_print [ "Print" "XML" identarg($id) "." ] ->
diff --git a/contrib/xml/ntrefiner.ml b/contrib/xml/ntrefiner.ml
deleted file mode 100644
index dd2b2ad942..0000000000
--- a/contrib/xml/ntrefiner.ml
+++ /dev/null
@@ -1,71 +0,0 @@
-(**************************************************************************
-  *********                  ntrefiner.ml                          *********
-  **************************************************************************)
-
-(*
-open Std;;
-open Names;;
-open Generic;;
-open Term;;
-open Termenv;;
-open More_util;;
-open Proof_trees;;
-open Logic;;
-open Refiner;;
-open Evd;;
-
-
-(*the only difference with extract_open_proof is that the 
-  path of the unsolved goal in put in metavar assoc list 
-  extract_open_proof : constr signature -> proof
-  -> constr * (int * constr) list
-  takes a constr signature corresponding to global definitions
-  and a (not necessarly complete) proof
-  and gives a pair (pfterm,obl)
-  where pfterm is the constr corresponding to the proof
-  and obl is an int*constr list [ (m1,c1) ; ... ; (mn,cn)]
-  where the mi are metavariables numbers, and ci are their types.
-  Their proof should be completed in order to complete the initial proof*)
-let nt_extract_open_proof sign pf =
- let open_obligations = ref [] in
- let st = Stack.create () in
- Stack.push 1 st;
- let rec proof_extractor vl =
-  function
-     | {ref=Some ((PRIM _), _)} as pf -> prim_extractor proof_extractor vl pf
-     | {ref=Some ((TACTIC (str, _)), spfl); subproof=Some hidden_proof} ->
-      let sgl, v = frontier hidden_proof in
-      let flat_proof = v spfl in
-      if str = "Interpret" then (Stack.push 1 st);
-       let c = proof_extractor vl flat_proof in
-       if str = "Interpret" then
-        (Stack.pop st; Stack.push ((Stack.pop st) + 1) st); c
-     | {ref=Some ((CONTEXT ctxt), (pf :: []))} -> (proof_extractor vl) pf
-     | {ref=Some ((LOCAL_CONSTRAINTS lc), (pf :: []))} ->
-      (proof_extractor vl) pf
-     | {ref=None; goal=goal} ->
-      let visible_rels = map_succeed (function id ->
-       (match lookup_id id vl with
-       | GLOBNAME _ -> failwith "caught"
-       | RELNAME (n, _) -> n, id)) (ids_of_sign goal.hyps) in
-      let
-      sorted_rels = Sort.list (fun (n1, _) (n2, _) -> n1>n2) visible_rels
-      in
-      let
-      abs_concl =
-       List.fold_right
-       (fun (_, id) concl -> mkNamedProd id (snd (lookup_sign id goal.hyps)) concl)
-       sorted_rels goal.concl in
-      let path =
-       let l = ref [] in
-       let f i = l:=i::!l in
-       Stack.iter f st; List.tl !l in
-      Stack.push ((Stack.pop st) + 1) st;
-       let mv = newMETA () in
-       open_obligations:=(mv, (abs_concl, path))::!open_obligations;
-       applist (DOP0 (Meta mv), List.map (function n, _ -> Rel n) sorted_rels)
-     | _ -> error "ntrfiner__nt_extract_open_proof" in
- let pfterm = proof_extractor (gLOB sign) pf in
- pfterm, List.rev !open_obligations;;
-
-*)
diff --git a/contrib/xml/ntrefiner.mli b/contrib/xml/ntrefiner.mli
deleted file mode 100644
index 1fb5bf1394..0000000000
--- a/contrib/xml/ntrefiner.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(**************************************************************************
-  *********                  ntrefiner.ml                          *********
-  **************************************************************************)
-(*
-open Names;;
-open Term;;
-open Proof_trees;;
-
-
-val nt_extract_open_proof : 
-  constr signature -> proof_tree -> 
-    constr * (int * (constr * int list)) list;;
-*)
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 *)