From 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Dec 2016 19:45:04 +0100
Subject: Passing around the flag for injection so that tactics calling inj at
 ML level can set the flags themselves.

In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".

This fixes bug #5281.
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 640ab4aa50..7a326c589a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,8 @@ Tactics
   such as "x := 5 : Z" (see BZ#148). This could be disabled via
   Unset Omega UseLocalDefs.
 - The tactic "romega" is also aware now of the bodies of context variables.
+- Tactic "decide equality" now able to manage constructors which
+  contain proofs.
 
 Changes from 8.7+beta2 to 8.7.0
 ===============================
-- 
cgit v1.2.3