aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-02 00:38:53 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-02 00:38:53 +0200
commitf79f2b32da8e5e443428d4f642216ddfb404857c (patch)
tree4c0a2a6cb8fba3cdaba833f612267a0cd81a5a5d /kernel
parent4f21c45748816c9e0cd4f93fa6f6d167e9757f81 (diff)
parentdef03f31c1c639629e6bb07e266319bf6930f8fb (diff)
Merge branch 'v8.6'
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml10
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 3864df6c9..ef4b50130 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1929,13 +1929,15 @@ let compile_constant env sigma prefix ~interactive con cb =
arg|])))::
[Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix
-let loaded_native_files = ref ([] : string list)
+module StringOrd = struct type t = string let compare = String.compare end
+module StringSet = Set.Make(StringOrd)
-let is_loaded_native_file s = String.List.mem s !loaded_native_files
+let loaded_native_files = ref StringSet.empty
+
+let is_loaded_native_file s = StringSet.mem s !loaded_native_files
let register_native_file s =
- if not (is_loaded_native_file s) then
- loaded_native_files := s :: !loaded_native_files
+ loaded_native_files := StringSet.add s !loaded_native_files
let is_code_loaded ~interactive name =
match !name with