From c6369bb7a5a4564d6fd77a2c04c24a1795e95bf9 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 14 Apr 2018 00:28:12 +0200
Subject: Add missing CHANGES entry for #6169.

Fixes #7243.
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 234d6c0dbf..9f4c71a563 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`
-- 
cgit v1.2.3