From 4a2e0798cf24c9edf4e96bd6ad62bdbde7a7cdf7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 3 Oct 2016 11:12:20 +0200
Subject: Document change related to Keep Proof Equalities in CHANGES.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index cf1fefa75d..a9ce5260a7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -69,6 +69,9 @@ Tactics
   hypotheses of the form "~True" or "t<>t" (possible source of
   incompatibilities because of more successes in automation, but
   generally a more intuitive strategy).
+- Option "Injection On Proofs" was renamed "Keep Proof Equalities". When
+  enabled, injection and inversion do not drop equalities between objects
+  in Prop. Still disabled by default.
 
 Hints
 
-- 
cgit v1.2.3