diff options
| author | letouzey | 2013-02-19 16:55:21 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-19 16:55:21 +0000 |
| commit | 81b527990c64a03a8b6942a7a0477e35ed144a76 (patch) | |
| tree | 318511d4a32088789259218b0343ffe778586909 /plugins | |
| parent | ef64634b31a4cd999cd08636adbf117f81889fb1 (diff) | |
Classops : avoid some use of Gmap
Gmap uses Pervasives.compare which may interact badly with
structures like pairs of kernel names
For the moment, we consider elements in classes and coercions only
according to their user kernel name: this provides maximal compatibility.
But it could be interesting to try using comparision according to
canonical kernel names...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16218 85f007b7-540e-0410-9357-904b9bb8a0f7
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] *) |