From 96bbe0590417d8885ac09abf7d749c12172e16bc Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 12 May 2017 10:58:26 +0200 Subject: Tests for new specialize feature + CHANGES. --- CHANGES | 3 +++ 1 file changed, 3 insertions(+) (limited to 'CHANGES') 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, -- cgit v1.2.3