From 81b527990c64a03a8b6942a7a0477e35ed144a76 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 19 Feb 2013 16:55:21 +0000 Subject: 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 --- library/globnames.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'library/globnames.ml') diff --git a/library/globnames.ml b/library/globnames.ml index 0ee82f0f7..02570d339 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 -- cgit v1.2.3