diff options
Diffstat (limited to 'contrib/xml/proof2aproof.ml')
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 2 |
1 files changed, 0 insertions, 2 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 |