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 ++
 pretyping/evd.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'pretyping')

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 =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 513ade646b..6c7ef2168c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -208,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t
 val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
 (** Compare the evar_info's up to the universe constraints of the evar map. *)
 
+val drop_all_defined : evar_map -> evar_map
+
 (** {6 Instantiating partial terms} *)
 
 exception NotInstantiatedEvar
-- 
cgit v1.2.3