From 1d3500af261d01ec552424c46311d49fe61c1300 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Apr 2017 16:35:19 +0200
Subject: Documenting the changes introduced by the EConstr branch.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 240d71ec04..f42239c794 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,17 @@ Tactics
 - New tactic "extensionality in H" which applies (possibly dependent)
   functional extensionality in H supposed to be a quantified equality
   until giving a bare equality.
+- New representation of terms that statically ensure stability by
+  evar-expansion. This has several consequences.
+  * In terms of performance, this adds a cost to every term destructuration,
+    but at the same time most eager evar normalizations were removed, which
+    couterbalances this drawback and even sometimes outperforms the old
+    implementation. For instance, many operations that would require O(n)
+    normalization of the term are now O(1) in tactics. YMMV.
+  * This triggers small changes in unification, which was not evar-insensitive.
+    Most notably, the new implementation recognizes Miller patterns that were
+    missed before because of a missing normalization step. Hopefully this should
+    be fairly uncommon.
 
 Standard Library
 
-- 
cgit v1.2.3