From 76f27140e6e3465b2d4086653bccae5206b3cfb6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 8 Sep 2015 13:06:27 +0200
Subject: Fixing clearing of temporary hypotheses with intro pattern
 pat/constr.

---
 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 661a786b0..3d6928d03 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2172,7 +2172,7 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
+                (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None []))
           sigma
       end
 
-- 
cgit v1.2.3