1 files changed, 0 insertions, 136 deletions
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
deleted file mode 100644
index 76364541..00000000
--- a/plugins/xml/dumptree.ml4
+++ /dev/null
@@ -1,136 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module provides the "Dump Tree" command that allows dumping the
-    current state of the proof stree in XML format *)
-
-(** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-open Tacexpr;;
-open Decl_mode;;
-open Printer;;
-open Pp;;
-open Environ;;
-open Format;;
-open Proof_type;;
-open Evd;;
-open Termops;;
-open Ppconstr;;
-open Names;;
-
-exception Different
-
-let xmlstream s =
-  (* In XML we want to print the whole stream so we can force the evaluation *)
-  Stream.of_list (List.map xmlescape (Stream.npeek max_int s))
-;;
-
-let thin_sign osign sign =
-  Sign.fold_named_context
-    (fun (id,c,ty as d) sign ->
-       try
-        if Sign.lookup_named id osign = (id,c,ty) then sign
-         else raise Different
-       with Not_found | Different -> Environ.push_named_context_val d sign)
-    sign ~init:Environ.empty_named_context_val
-;;
-
-let pr_tactic_xml = function
-  | TacArg (_,Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>"
-  | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>"
-;;
-
-let pr_proof_instr_xml instr =
-  Ppdecl_proof.pr_proof_instr (Global.env()) instr
-;;
-
-let pr_rule_xml pr = function
-  | Prim r -> str "<rule text=\"" ++ xmlstream (pr_prim_rule r) ++ str "\"/>"
-  | Nested(cmpd, subtree) ->
-      hov 2 (str "<cmpdrule>" ++ fnl () ++
-        begin match cmpd with
-          Tactic (texp, _) -> pr_tactic_xml texp
-        end ++ fnl ()
-        ++ pr subtree
-      ) ++ fnl () ++ str "</cmpdrule>"
-  | Daimon -> str "<daimon/>"
-  | Decl_proof _ -> str "<proof/>"
-;;
-
-let pr_var_decl_xml env (id,c,typ) =
-  let ptyp = print_constr_env env typ in
-  match c with
-  | None ->
-      (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\"/>")
-  | Some c ->
-      (* Force evaluation *)
-      let pb = print_constr_env env c in
-      (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\" body=\"" ++
-         xmlstream pb ++ str "\"/>")
-;;
-
-let pr_rel_decl_xml env (na,c,typ) =
-  let pbody = match c with
-    | None -> mt ()
-    | Some c ->
-	(* Force evaluation *)
-	let pb = print_constr_env env c in
-	  (str" body=\"" ++ xmlstream pb ++ str "\"") in
-  let ptyp = print_constr_env env typ in
-  let pid =
-    match na with
-    | Anonymous -> mt ()
-    | Name id -> str " id=\"" ++ pr_id id ++ str "\""
-  in
-  (str "<hyp" ++ pid ++ str " type=\"" ++ xmlstream ptyp ++ str "\"" ++ pbody ++ str "/>")
-;;
-
-let pr_context_xml env =
-  let sign_env =
-    fold_named_context
-      (fun env d pp -> pp ++ pr_var_decl_xml env d)
-      env ~init:(mt ())
-  in
-  let db_env =
-    fold_rel_context
-      (fun env d pp -> pp ++ pr_rel_decl_xml env d)
-      env ~init:(mt ())
-  in
-  (sign_env ++ db_env)
-;;
-
-let pr_subgoal_metas_xml metas env=
-  let pr_one (meta, typ) =
-    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++
-      str "\"/>"
-  in
-  List.fold_left (++) (mt ()) (List.map pr_one metas)
-;;
-
-let pr_goal_xml sigma g =
-  let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
-  if Decl_mode.try_get_info sigma g = None then
-    (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
-    xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++
-    str "\"/>" ++
-    (pr_context_xml env)) ++
-    fnl () ++ str "</goal>")
-  else
-    (hov 2 (str "<goal type=\"declarative\">" ++
-    (pr_context_xml env)) ++
-    fnl () ++ str "</goal>")
-;;
-
-let print_proof_xml () =
-  Util.anomaly "Dump Tree command not supported in this version."
-
-
-VERNAC COMMAND EXTEND DumpTree
-  [ "Dump" "Tree" ] -> [ print_proof_xml () ]
-END