diff options
| -rw-r--r-- | proofs/proof.ml | 15 | ||||
| -rw-r--r-- | proofs/proof.mli | 4 |
2 files changed, 1 insertions, 18 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 71afae0204..bae5f11576 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -121,8 +121,6 @@ type proof_state = { to unfocus the proof and the extra information stored while focusing. The list is empty when the proof is fully unfocused. *) focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list; - (* Extra information which can be freely used to create new behaviours. *) - intel: Store.t } type proof_info = { @@ -379,8 +377,7 @@ let unfocused = is_last_focus end_of_stack_kind let start goals = let pr = { state = { proofview = Proofview.init goals ; - focus_stack = [] ; - intel = Store.empty} ; + focus_stack = [] }; undo_stack = [] ; transactions = [] ; info = { endline_tactic = Proofview.tclUNIT (); @@ -408,16 +405,6 @@ let return p = unfocus end_of_stack_kind p; Proofview.return p.state.proofview -(*** Function manipulation proof extra informations ***) - -let get_proof_info pr = - pr.state.intel - -let set_proof_info info pr = - save pr; - pr.state <- { pr.state with intel=info } - - (*** Tactics ***) let run_tactic env tac pr = diff --git a/proofs/proof.mli b/proofs/proof.mli index 2d570c53ac..7d82ee91e7 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -138,10 +138,6 @@ val is_last_focus : 'a focus_kind -> proof -> bool (* returns [true] if there is no goal under focus. *) val no_focused_goal : proof -> bool -(*** Function manipulation proof extra informations ***) - -val get_proof_info : proof -> Store.t - (* Sets the section variables assumed by the proof *) val set_used_variables : Sign.section_context -> proof -> unit val get_used_variables : proof -> Sign.section_context option |