new: Optimize Proof, Optimize Heap

- drops all Defined entries from the evar map (applying the subst to the
  initial evar and the undefined evars types).
- call Gc.compact

Now the question is: where should these two commands be documented?

1 files changed, 3 insertions, 0 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 29828bbbe7..796a6a7baa 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -32,6 +32,9 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map
 (** Abstract representation of the initial goals of a proof. *)
 type entry
 
+(** Optimize memory consumption *)
+val compact : entry -> proofview -> entry * proofview
+
 (** Initialises a proofview, the main argument is a list of
     environements (including a [named_context] which are used as
     hypotheses) pair with conclusion types, creating accordingly many