diff options
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 |