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

---
 tactics/tactics.ml          |  2 +-
 test-suite/success/intros.v | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2e7adc513..0c4c5b673 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2240,7 +2240,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
   | IntroInjection l' ->
       intro_decomp_eq loc l' thin tac id
   | IntroRewrite l2r ->
-      Tacticals.New.tclTHENLAST
+      Tacticals.New.tclTHENFIRST
         (* Skip the side conditions of the rewriting step *)
 	(rewrite_hyp style l2r id)
         (tac thin None [])
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 11156aa0e..69d66f100 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