diff options
Diffstat (limited to 'contrib/xml/proofTree2Xml.ml4')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 578c1ed2..dbdc79a8 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) | {PT.goal=goal; - PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} -> + 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] *) @@ -194,6 +194,12 @@ Pp.ppnl (Pp.(++) (Pp.str (List.fold_left (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) + | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} -> + Util.anomaly "Not Implemented" + + | {PT.ref=Some(PT.Daimon,_)} -> + X.xml_empty "Hidden_open_goal" of_attribute + | {PT.ref=None;PT.goal=goal} -> X.xml_empty "Open_goal" of_attribute in |