diff options
| author | Hugo Herbelin | 2016-06-07 16:00:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-07 16:03:49 +0200 |
| commit | 08c69c4dd28f9e4c7a536f32e5efacc23973a71a (patch) | |
| tree | 23fc9050ea5b0942637376050071d29a97ecdac3 | |
| parent | 33f7d95a655add1967b5c520eb05e816963e1936 (diff) | |
Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files 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] |