From ce80fa3cb3e6d8809bb3ee015bff39c67c0aed16 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 9 Nov 2014 19:44:17 +0100
Subject: 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?
---
 proofs/proof.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index be23d77296..c55e562a2b 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.
-- 
cgit v1.2.3