From 0dd54498c41ddd2dc0a4cbfdef723cecfa6a0605 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 10 Jan 2015 11:01:03 +0100
Subject: CHANGES: mention "Optimize (Heap|Proof)"

---
 CHANGES | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGES b/CHANGES
index daea9f2593..bccb85e8a1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,6 +73,12 @@ Vernacular commands
 - "Collection" command to name sets of section hypotheses.  Named collections
   can be used in the syntax of "Proof using" to assert with section variables
   are used in a proof.
+- The "Optimize Proof" command can be placed in the middle of a proof to
+  force the compaction the data structure used to represent the ongoing
+  proof (evar map).  This may result in a lower memory footprint and speed up
+  the execution of the following tactics.
+- "Optimize Heap" command to tell the OCaml runtime to performa a major
+  garbage collection step and heap compaction.
 
 Specification Language
 
-- 
cgit v1.2.3