From 0746578040e738d079bcc3289857bb99983a7a22 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 30 Sep 2016 11:52:21 +0200
Subject: fixing bug 4609: document an option governing the generation of
 equalities between proofs in tactic injection, with a side-effect on
 inversion.

---
 test-suite/success/Injection.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 8745cf2fbd..da2183841d 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -135,6 +135,21 @@ intros * [= H].
 exact H.
 Abort.
 
+(* Test the Keep Proof Equalities option. *)
+Set Keep Proof Equalities.
+Unset Structural Injection.
+
+Inductive pbool : Prop := Pbool1 | Pbool2.
+
+Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell.
+
+Goal Pbsc Pbool1 = Pbsc Pbool2 -> True.
+injection 1.
+match goal with
+ |- Pbool1 = Pbool2 -> True => idtac | |- True => fail
+end.
+Abort.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
-- 
cgit v1.2.3