diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 08:30:48 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 08:30:48 +0200 |
| commit | df093d928ea09c5a4c5212cdb837da55d833760d (patch) | |
| tree | bc88a1674663f5976d180d0cd24249024bc4116b | |
| parent | 4c466c429902d0ef0bd0da0f42e1a3b6d9f7d32a (diff) | |
| parent | c6369bb7a5a4564d6fd77a2c04c24a1795e95bf9 (diff) | |
Merge PR #7246: Add missing CHANGES entry for #6169.
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -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` |