diff options
| author | Maxime Dénès | 2017-10-03 11:45:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-03 11:45:31 +0200 |
| commit | afe519db64b4864b5a901ab96a1e4297e9316b14 (patch) | |
| tree | 9fe22a04fcfd049081dedb6f9262a3a321176d03 /plugins/extraction/extraction.ml | |
| parent | e33cd69ab6fcb38478a6c0e00628a5de16181906 (diff) | |
| parent | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (diff) | |
Merge PR #1040: Efficient fresh name generation
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 7644b49ceb..a227478d0f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -141,6 +141,7 @@ let make_typvar n vl = if not (String.contains s '\'') && Unicode.is_basic_ascii s then id else id_of_name Anonymous in + let vl = Id.Set.of_list vl in next_ident_away id' vl let rec type_sign_vl env c = |