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?
---
 pretyping/evd.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/evd.ml')

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 =
-- 
cgit v1.2.3