diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bbee0a2a79..0235126cc0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2122,7 +2122,7 @@ let make_tmp_naming avoid l = function case of IntroFresh, we should use check_thin_clash_then anyway to prevent the case of an IntroFresh precisely using the wild_id *) | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l) - | _ -> NamingAvoid(avoid@explicit_intro_names l) + | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l)) let fit_bound n = function | None -> true |