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

5 files changed, 2 insertions, 37 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 4652bac2ed..d806d80b88 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -40,14 +40,7 @@ type prim_rule =
   | Rename of identifier * identifier
   | Change_evars
 
-type proof_tree = {
-  goal : goal;
-  ref : (rule * proof_tree list) option }
-
-and rule =
-  | Prim of prim_rule
-  | Decl_proof of bool
-  | Daimon
+type rule = Prim of prim_rule
 
 type compound_rule=
   | Tactic of tactic_expr * bool
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index d6081e56c3..832377e316 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -66,21 +66,7 @@ type prim_rule =
                                               in the type of evar] \} \} \} v}
 *)
 
-(** {6 ... } *)
-(** Proof trees.
-  [ref] = [None] if the goal has still to be proved,
-  and [Some (r,l)] if the rule [r] was applied to the goal
-  and gave [l] as subproofs to be completed.
-  if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
-  that the goal can be proven if the goals in [l] are solved. *)
-type proof_tree = {
-  goal : goal;
-  ref : (rule * proof_tree list) option }
-
-and rule =
-  | Prim of prim_rule
-  | Decl_proof of bool
-  | Daimon
+type rule = Prim of prim_rule
 
 type compound_rule=
   (** the boolean of Tactic tells if the default tactic is used *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 87ba77dc52..9b9b913375 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -35,16 +35,6 @@ let refiner = function
 	  {it=sgl; sigma = sigma'})
 
 
-  | Decl_proof _ ->
-      failwith "Refiner: should not occur"
-
-	(* Daimon is a canonical unfinished proof *)
-
-  | Daimon ->
-      fun gls ->
-	{it=[];sigma=gls.sigma}
-
-
 let norm_evar_tac gl = refiner (Prim Change_evars) gl
 
 (*********************)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4524fe6a16..80a450bcd6 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -109,8 +109,6 @@ let pf_matches                  = pf_apply Matching.matches_conv
 (* Tactics handling a list of goals *)
 (************************************)
 
-type validation_list = proof_tree list -> proof_tree list
-
 type tactic_list = Refiner.tactic_list 
 
 let first_goal         = first_goal
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e7ad5d000d..da9aecde9e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -118,8 +118,6 @@ val rename_hyp       : (identifier*identifier) list -> tactic
 
 (** {6 Tactics handling a list of goals. } *)
 
-type validation_list = proof_tree list -> proof_tree list
-
 type tactic_list = Refiner.tactic_list
 
 val first_goal         : 'a list sigma -> 'a sigma