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.
---
 dev/doc/changes.md | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 8a2a2fffc6..6ade6576f7 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -32,6 +32,12 @@ We renamed the following datatypes:
 
 - `Pp.std_ppcmds` -> `Pp.t`
 
+Some tactics and related functions now support static configurability, e.g.:
+
+- injectable, dEq, etc. takes an argument ~keep_proofs which,
+  - if None, tells to behave as told with the flag Keep Proof Equalities
+  - if Some b, tells to keep proof equalities iff b is true
+
 ## Changes between Coq 8.6 and Coq 8.7
 
 ### Ocaml
-- 
cgit v1.2.3