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_global.mli b/proofs/proof_global.mli
index de259a4cc..8dd739686 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,6 +46,8 @@ exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 (** @raise NoCurrentProof when outside proof mode. *)
 
+val compact_the_proof : unit -> unit
+
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
     (in a form suitable for definitions). Together with the [terminator]