diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-22 18:06:35 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-22 18:06:35 +0000 |
commit | 90a2cea28df5ecdf9e2cdc4351aad5f6a993a003 (patch) | |
tree | b9994cf9ff1163facd312b96918d929f5e0ff7ae /contrib/xml | |
parent | 612ea3d4b3c7d7e00616b009050803cd7b7f763e (diff) |
Correction du bug #1315:
- ajouts des opérations clear_evar_hyps_in_evar,
clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui
permettent de supprimer des hypothèses dans le contexte des evars,
en créant une nouvelle evar avec un contexte restreint;
- adaptation de clear_hyps dans Logic pour qu'elle mette à jour le
contexte des evars;
- adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié;
- déplacement de la tactique Change_evars dans prim_rule.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
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 92cbf6df5..30dc7b710 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 dbdc79a80..9afd07a61 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" |