ntrefiner.ml* removed in module xml

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

7 files changed, 22 insertions, 105 deletions

diff --git a/.depend b/.depend
index d1c9086d88..87b042eb77 100644
--- a/.depend
+++ b/.depend
@@ -928,10 +928,8 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
-tools/coqdep_lexer.cmo: config/coq_config.cmi 
-tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi 
+tools/coqdep.cmx: config/coq_config.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \
@@ -1136,23 +1134,25 @@ contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
     library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
     tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx 
-contrib/xml/cooking.cmo: kernel/names.cmi kernel/term.cmi \
+contrib/xml/cooking.cmo: kernel/declarations.cmi library/global.cmi \
+    kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
     contrib/xml/cooking.cmi 
-contrib/xml/cooking.cmx: kernel/names.cmx kernel/term.cmx \
+contrib/xml/cooking.cmx: kernel/declarations.cmx library/global.cmx \
+    kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
     contrib/xml/cooking.cmi 
-contrib/xml/ntrefiner.cmo: contrib/xml/ntrefiner.cmi 
-contrib/xml/ntrefiner.cmx: contrib/xml/ntrefiner.cmi 
 contrib/xml/xml.cmo: contrib/xml/xml.cmi 
 contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/cooking.cmi kernel/declarations.cmi \
-    library/declare.cmi library/global.cmi library/lib.cmi \
+    library/declare.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
-    library/nametab.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
+    library/nametab.cmi proofs/pfedit.cmi proofs/proof_trees.cmi \
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlcommand.cmx: contrib/xml/cooking.cmx kernel/declarations.cmx \
-    library/declare.cmx library/global.cmx library/lib.cmx \
+    library/declare.cmx kernel/evd.cmx library/global.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
-    library/nametab.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
+    library/nametab.cmx proofs/pfedit.cmx proofs/proof_trees.cmx \
+    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
     contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
     contrib/xml/xmlcommand.cmi 
diff --git a/.depend.coq b/.depend.coq
index fbb0a9bc01..bf1435e813 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -94,7 +94,7 @@ theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Ar
 test-suite/tactics/TestRefine.vo: test-suite/tactics/TestRefine.v tactics/Refine.vo theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Arith/Lt.vo
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
-contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/ntrefiner.cmo contrib/xml/xml.cmo contrib/xml/cooking.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
+contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/cooking.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
diff --git a/Makefile b/Makefile
index 3c7e98f07c..945e7bd606 100644
--- a/Makefile
+++ b/Makefile
@@ -121,7 +121,7 @@ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
         contrib/ring/quote.cmo contrib/ring/ring.cmo \
         contrib/xml/xml.cmo contrib/xml/cooking.cmo contrib/xml/xmlcommand.cmo \
-        contrib/xml/xmlentries.cmo contrib/xml/ntrefiner.cmo
+        contrib/xml/xmlentries.cmo
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
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 *)