aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2017-05-12 10:58:26 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2017-05-31 11:27:15 +0200
commit96bbe0590417d8885ac09abf7d749c12172e16bc (patch)
tree75e19acb72216ea2784a5464133032638d78dbaf /CHANGES
parent0e37dc665cf7a6a9ed7d0d10199dd40134cf0148 (diff)
Tests for new specialize feature + CHANGES.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 30bea7a7b..847073eaf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,9 @@ 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.
+- Tactic "specialize with ..." now accepts any partial bindings.
+ Missing bindings are either solved by unification or left quantified
+ in the hypothesis.
- 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,