diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 11:45:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 11:45:31 +0200 |
| commit | afe519db64b4864b5a901ab96a1e4297e9316b14 (patch) | |
| tree | 9fe22a04fcfd049081dedb6f9262a3a321176d03 /pretyping/constr_matching.ml | |
| parent | e33cd69ab6fcb38478a6c0e00628a5de16181906 (diff) | |
| parent | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (diff) | |
Merge PR #1040: Efficient fresh name generation
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ca7f633dc..0973d73ee 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -178,7 +178,7 @@ let push_binder na1 na2 t ctx = let id2 = match na2 with | Name id2 -> id2 | Anonymous -> - let avoid = List.map pi2 ctx in + let avoid = Id.Set.of_list (List.map pi2 ctx) in Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in (na1, id2, t) :: ctx |