diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 9252ae0ec8..320e0d1fca 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -24,8 +24,8 @@ open Miniml (** Sets and maps for [global_reference] that use the "user" [kernel_name] instead of the canonical one *) -module Refmap' = Map.Make(RefOrdered_env) -module Refset' = Set.Make(RefOrdered_env) +module Refmap' = Refmap_env +module Refset' = Refset_env (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) |