diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-08 14:19:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-08 14:19:34 +0200 |
| commit | 7e00e8d602e67810700a7071c419ffd7ef8806c5 (patch) | |
| tree | 0541e014fc1bf128bb13a816c31d1d4ceb18f51c /tactics | |
| parent | 11fc2695936c4cff0eea18cb97f6c83eb7cff09d (diff) | |
Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits
ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).
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 bbee0a2a7..0235126cc 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 |