6 files changed, 8 insertions, 7 deletions
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index fabe9a4c67..09b0444614 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -34,4 +34,4 @@ Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
 Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
 Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
 Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
-\ No newline at end of file
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index fe6eb7780f..ab13d75ada 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -96,4 +96,4 @@ Extraction "/tmp/test.ml"
   pos_of_int int_of_pos
   z_of_int int_of_z
   n_of_int int_of_n.
-*)
-\ No newline at end of file
+*)
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
index 1374a91abf..b3f9d6556d 100644
--- a/plugins/extraction/Extraction.v
+++ b/plugins/extraction/Extraction.v
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Declare ML Module "extraction_plugin".
-\ No newline at end of file
+Declare ML Module "extraction_plugin".
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9772ebd641..9aec190d0a 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     match l with
     | [""] -> (* this happens only at toplevel of the monolithic case *)
-      let globs = Id.Set.elements (get_global_ids ()) in
+      let globs = get_global_ids () in
       let id = next_ident_away (kindcase_id k idg) globs in
       Id.to_string id
     | _ -> modular_rename k idg
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 =
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ca98f07e8d..30e3b520f9 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -750,11 +750,11 @@ let extraction_implicit r l =
 
 let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
 
-let modfile_ids = ref []
+let modfile_ids = ref Id.Set.empty
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Id.Set.elements !blacklist_table;
+  modfile_ids := !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
@@ -763,7 +763,7 @@ let string_of_modfile mp =
     let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
     let s' = Id.to_string id' in
-    modfile_ids := id' :: !modfile_ids;
+    modfile_ids := Id.Set.add id' !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'