diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:24 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:24 +0000 |
commit | 8e10368c387570df13904531bfba05130335ed0e (patch) | |
tree | 50d7a35c9a45e0c9496da4a4ad22ead531be829d /plugins/xml | |
parent | 2e3cf396ba869987c4e41f46bc9b4b2fe31ab4d2 (diff) |
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
Diffstat (limited to 'plugins/xml')
-rw-r--r-- | plugins/xml/dumptree.ml4 | 7 | ||||
-rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 51 |
2 files changed, 0 insertions, 58 deletions
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 623d7c804..c29e4a3b3 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 033e83410..3831ee9fa 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 |