From e1cf5ccd8df7080d7dd2aadf0305a9d3ba9c5d9d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 18 May 2014 13:03:54 -0400
Subject: Restored old behavior of injection on proofs by default.

Use Set Injection On Proof to enable the new behavior.
---
 CHANGES | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 2dd953bf33..66d5a0e0f7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -104,9 +104,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.
+- Injection can now also deduce equality of arguments of sort Prop, by using
+  the option "Set Injection On Proofs" (disabled by default). Also improved the
+  error messages.
 - Tactic "subst id" now supports id occurring in dependent local definitions.
 
 Program
-- 
cgit v1.2.3