diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-02 00:38:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-02 00:38:53 +0200 |
| commit | f79f2b32da8e5e443428d4f642216ddfb404857c (patch) | |
| tree | 4c0a2a6cb8fba3cdaba833f612267a0cd81a5a5d /kernel | |
| parent | 4f21c45748816c9e0cd4f93fa6f6d167e9757f81 (diff) | |
| parent | def03f31c1c639629e6bb07e266319bf6930f8fb (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 10 |
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 |