diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 7f076db2a924377e9de3f9a6d838b8c44ed2e16d (patch) | |
tree | e075c526532a227c83d951c9dff8c944ea0c4d15 /contrib/xml | |
parent | 2a14f39fdfa80b021227396b22e38ed7c35356df (diff) | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Merge commit 'upstream/8.1+dfsg' into 8.1
Diffstat (limited to 'contrib/xml')
-rw-r--r-- | contrib/xml/proof2aproof.ml | 2 | ||||
-rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 7 |
2 files changed, 1 insertions, 8 deletions
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 92cbf6df..30dc7b71 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -112,8 +112,6 @@ let extract_open_proof sigma pf = ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ; proof_extractor vl flat_proof - | {PT.ref=Some(PT.Change_evars,[pf])} -> (proof_extractor vl) pf - | {PT.ref=None;PT.goal=goal} -> let visible_rels = Util.map_succeed 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" |