From c3e01a044297d322d8a5e6830fe3af002ebd2dce Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Dec 2015 08:23:35 +0100
Subject: Fixing an "injection as" bug in the presence of side conditions.

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

(limited to 'test-suite')

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 25e464d677..8fd0394625 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -68,6 +68,12 @@ einjection (H O).
 instantiate (1:=O).
 Abort.
 
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+einjection (H O) as H0.
+instantiate (y:=O).
+Abort.
+
 (* Test the injection intropattern *)
 
 Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b.
-- 
cgit v1.2.3