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, 4 insertions, 0 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index abd1024d6e..5654e464ad 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -312,6 +312,10 @@ let return p =
 
 let initial_goals p = Proofview.initial_goals p.entry
 
+let compact p =
+  let entry, proofview = Proofview.compact p.entry p.proofview in
+  { p with proofview; entry }
+
 (*** Function manipulation proof extra informations ***)
 
 (*** Tactics ***)