diff options
Diffstat (limited to 'contrib/xml/proofTree2Xml.ml4')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index dbdc79a8..9afd07a6 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -93,7 +93,7 @@ let string_of_prim_rule x = match x with | Proof_type.ThinBody _-> "ThinBody" | Proof_type.Move (_,_,_) -> "Move" | Proof_type.Rename (_,_) -> "Rename" - + | Proof_type.Change_evars -> "Change_evars" let print_proof_tree curi sigma pf proof_tree_to_constr @@ -189,11 +189,6 @@ Pp.ppnl (Pp.(++) (Pp.str [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>] end - | {PT.ref=Some(PT.Change_evars,nodes)} -> - X.xml_nempty "Change_evars" of_attribute - (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" |