aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES3
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 234d6c0db..9f4c71a56 100644
--- a/CHANGES
+++ b/CHANGES
@@ -93,6 +93,7 @@ Tactics
of the execution.
- `vm_compute` now supports existential variables.
- Calls to `shelve` and `give_up` within calls to tactic `refine` now working.
+- Deprecated tactic `appcontext` was removed.
Focusing
@@ -196,6 +197,7 @@ Options
+ `Refolding Reduction`
+ `Standard Proposition Elimination`
+ + `Dependent Propositions Elimination`
+ `Discriminate Introduction`
+ `Shrink Abstract`
+ `Tactic Pattern Unification`
@@ -203,6 +205,7 @@ Options
+ `Injection L2R Pattern Order`
+ `Record Elimination Schemes`
+ `Match Strict`
+ + `Tactic Compat Context`
+ `Typeclasses Legacy Resolution`
+ `Typeclasses Module Eta`
+ `Typeclass Resolution After Apply`