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

diff --git a/proofs/proof.mli b/proofs/proof.mli
index be23d7729..c55e562a2 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -77,6 +77,8 @@ val is_done : proof -> bool
 (* Returns the list of partial proofs to initial goals. *)
 val partial_proof : proof -> Term.constr list
 
+val compact : proof -> proof
+
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
     Raises [HasShelvedGoals] if some goals are left on the shelf.