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.
---
 test-suite/bugs/closed/5281.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/5281.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5281.v b/test-suite/bugs/closed/5281.v
new file mode 100644
index 0000000000..03bafdc9ae
--- /dev/null
+++ b/test-suite/bugs/closed/5281.v
@@ -0,0 +1,6 @@
+Inductive A (T : Prop) := B (_ : T).
+Scheme Equality for A.
+
+Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}.
+decide equality.
+Qed.
-- 
cgit v1.2.3