From 3092819d4e3e1d0995c8156be0b98dce0afbcb9a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 30 Apr 2014 01:02:39 -0400
Subject: Document changes on injection.

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

diff --git a/CHANGES b/CHANGES
index 8adda60390..15adc5a5c6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -74,6 +74,9 @@ Tactics
   former behavior obtainable by "Unset Injection L2R Pattern Order").
 - New tactic "rewrite_strat" for generalized rewriting with user-defined
   strategies, subsumming autorewrite.
+- Injection now also deduces equality of arguments of sort Prop. Old behavior
+  can be restored by "Unset Injection On Proofs". Also improved the error
+  messages.
 
 Program
 
-- 
cgit v1.2.3