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 /library | |
| 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 'library')
| -rw-r--r-- | library/globnames.ml | 5 | ||||
| -rw-r--r-- | library/globnames.mli | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 0ee82f0f78..02570d3398 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -103,6 +103,11 @@ end module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) +(* Alternative sets and maps indexed by the user part of the kernel names *) + +module Refset_env = Set.Make(RefOrdered_env) +module Refmap_env = Map.Make(RefOrdered_env) + (* Extended global references *) type syndef_name = kernel_name diff --git a/library/globnames.mli b/library/globnames.mli index 1e6f143cd3..1e53186f4d 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -59,6 +59,9 @@ end module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference +module Refset_env : Set.S with type elt = global_reference +module Refmap_env : Map.S with type key = global_reference + (** {6 Extended global references } *) type syndef_name = kernel_name |