aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorletouzey2012-10-06 10:08:27 +0000
committerletouzey2012-10-06 10:08:27 +0000
commit4a8188a2b460ab014379c508abac933690b48555 (patch)
tree5e80d9c7f9b15d9fc3143f42fd0f61e8e1c3da09 /dev
parent8e10368c387570df13904531bfba05130335ed0e (diff)
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
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib1
-rw-r--r--dev/top_printers.ml1
2 files changed, 0 insertions, 2 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f065304422..8e72580629 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -144,7 +144,6 @@ Pcoq
Printer
Pptactic
Ppdecl_proof
-Tactic_printer
Egramml
Egramcoq
Himsg
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e65e418478..8e7a92a8ff 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -20,7 +20,6 @@ open Sign
open Univ
open Environ
open Printer
-open Tactic_printer
open Term
open Termops
open Cerrors