From df9d69f3ccf3e5600919a21112afda00b463fbc5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Dec 2015 19:38:19 +0100
Subject: Fixing a bug in the order of side conditions for introduction pattern
 -> and <-.

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

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 11156aa0ee..69d66f1008 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -84,3 +84,17 @@ Qed.
 Goal forall x : nat, True.
 intros y%(fun x => x).
 Abort.
+
+(* Fixing a bug in the order of side conditions of a "->" step *)
+
+Goal (True -> 1=0) -> 1=1.
+intros ->.
+- reflexivity.
+- exact I.
+Qed.
+
+Goal forall x, (True -> x=0) -> 0=x.
+intros x ->.
+- reflexivity.
+- exact I.
+Qed.
-- 
cgit v1.2.3