Remove the unused "intel" field in Proof.proof_state

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15846 85f007b7-540e-0410-9357-904b9bb8a0f7

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