From 4a8188a2b460ab014379c508abac933690b48555 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 6 Oct 2012 10:08:27 +0000
Subject: Clean-up : no more Proof_type.proof_tree

 Btw, remove unused code in the xml plugin and in Tactic_printer

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/xmlcommand.ml | 34 +++-------------------------------
 1 file changed, 3 insertions(+), 31 deletions(-)

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

diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 2550e248af..0673e79fb0 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -16,21 +16,6 @@
 
 let verbose = ref false;;
 
-(* HOOKS *)
-let print_proof_tree, set_print_proof_tree =
- let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in
-  (fun () -> !print_proof_tree),
-   (fun f ->
-     print_proof_tree :=
-     fun
-      curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree
-      constr_to_ids
-     ->
-      Some
-       (f curi sigma0 pf proof_tree_to_constr
-        proof_tree_to_flattened_proof_tree constr_to_ids))
-;;
-
 (* UTILITY FUNCTIONS *)
 
 let print_if_verbose s = if !verbose then print_string s;;
@@ -139,7 +124,7 @@ let theory_filename xml_library_root =
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
 
-let print_object uri obj sigma proof_tree_infos filename =
+let print_object uri obj sigma filename =
  (* function to pretty print and compress an XML file *)
 (*CSC: Unix.system "gzip ..." is an horrible non-portable solution. *)
  let pp xml filename =
@@ -169,20 +154,7 @@ let print_object uri obj sigma proof_tree_infos filename =
       None -> ()
     | Some xml' -> pp xml' (body_filename_of_filename filename)
   end ;
-  pp xmltypes (types_filename_of_filename filename) ;
-  match proof_tree_infos with
-     None -> ()
-   | Some (sigma0,proof_tree,proof_tree_to_constr,
-           proof_tree_to_flattened_proof_tree) ->
-      let xmlprooftree =
-       print_proof_tree ()
-        uri sigma0 proof_tree proof_tree_to_constr
-        proof_tree_to_flattened_proof_tree constr_to_ids
-      in
-       match xmlprooftree with
-          None -> ()
-        | Some xmlprooftree ->
-           pp xmlprooftree (prooftree_filename_of_filename filename)
+  pp xmltypes (types_filename_of_filename filename)
 ;;
 
 let string_list_of_named_context_list =
@@ -445,7 +417,7 @@ let print internal glob_ref kind xml_library_root =
   (match internal with
     | Declare.KernelSilent -> ()
     | _ -> print_object_kind uri kind);
-   print_object uri obj Evd.empty None fn
+   print_object uri obj Evd.empty fn
 ;;
 
 let print_ref qid fn =
-- 
cgit v1.2.3