From 8e10368c387570df13904531bfba05130335ed0e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 6 Oct 2012 10:08:24 +0000
Subject: Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box

 Nested was never constructed, while the notion of abstract_tactic_box
 is obsolete (cf. Refiner.abstract_tactic).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/dumptree.ml4      |  7 ------
 plugins/xml/proofTree2Xml.ml4 | 51 -------------------------------------------
 2 files changed, 58 deletions(-)

(limited to 'plugins/xml')

diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 623d7c8049..c29e4a3b3f 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -47,13 +47,6 @@ let pr_proof_instr_xml 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/>"
 ;;
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 033e834101..3831ee9fa4 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -113,57 +113,6 @@ Pp.msg_warning (Pp.(++) (Pp.str
             (List.fold_left
               (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
-     | {PT.goal=goal;
-        PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} ->
-         (* [hidden_proof] is the proof of the tactic;                     *)
-         (* [nodes] are the proof of the subgoals generated by the tactic; *)
-         (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
-         (*  for the holes in [hidden_proof]                               *)
-        let flat_proof =
-         Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
-        in begin
-        match tactic_expr with
-        | Tacexpr.TacArg (_,Tacexpr.Tacexp _) ->
-            (* We don't need to keep the level of abstraction introduced at *)
-            (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
-            aux flat_proof old_hyps
-        | _ ->
-         (****** la tactique employee *)
-	 let prtac = Pptactic.pr_tactic (Global.env()) in
-         let tac = Pp.string_of_ppcmds (prtac tactic_expr) in
-         let tacname= first_word tac in
-         let of_attribute = ("name",tacname)::("script",tac)::of_attribute in
-
-         (****** le but *)
-
-	 let concl = Goal.V82.concl sigma goal in
-	 let hyps = Goal.V82.hyps sigma goal in
-
-         let env = Global.env_of_context hyps in
-	   
-
-         let xgoal =
-          X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
-
-         let rec build_hyps =
-          function
-           | [] -> xgoal
-           | (id,c,tid)::hyps1 ->
-              let id' = Names.string_of_id id in
-               [< build_hyps hyps1;
-                  (X.xml_nempty "Hypothesis"
-                    ["id",idref_of_id id' ; "name",id']
-                    (constr_to_xml tid sigma env))
-               >] in
-         let old_names = List.map (fun (id,c,tid)->id) old_hyps in
-	 let nhyps = Environ.named_context_of_val hyps in
-         let new_hyps =
-          List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in
-
-         X.xml_nempty "Tactic" of_attribute
-          [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
-        end
-
      | {PT.ref=Some(PT.Daimon,_)} ->
          X.xml_empty "Hidden_open_goal" of_attribute
 
-- 
cgit v1.2.3