diff options
Diffstat (limited to 'plugins/xml/proofTree2Xml.ml4')
| -rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 51 |
1 files changed, 0 insertions, 51 deletions
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 |