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/pretyping/evd.ml b/pretyping/evd.ml
index ab595be25b..d36a6a20fb 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -655,6 +655,8 @@ let to_list d =
 
 let undefined_map d = d.undf_evars
 
+let drop_all_defined d = { d with defn_evars = EvMap.empty }
+
 (* spiwack: not clear what folding over an evar_map, for now we shall
     simply fold over the inner evar_map. *)
 let fold f d a =