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 <-.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2e7adc513a..0c4c5b673b 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 [])
-- 
cgit v1.2.3