From 08c69c4dd28f9e4c7a536f32e5efacc23973a71a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Jun 2016 16:00:51 +0200
Subject: Fixing #4787 (Unset Bracketing Last Introduction Pattern not
 working).

---
 tactics/tactics.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 75273e4b7b..858cc482ae 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2453,9 +2453,10 @@ let intro_patterns_bound_to n destopt =
   intro_patterns_core true [] [] [] destopt
     (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
 
-let intro_patterns_to destopt =
+let intro_patterns_to destopt l =
+  (* Eta-expansion because of a side-effect *)
   intro_patterns_core (use_bracketing_last_or_and_intro_pattern ())
-    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
+    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) l
 
 let intro_pattern_to destopt pat =
   intro_patterns_to destopt [dloc,pat]
-- 
cgit v1.2.3