diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 16:55:21 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 16:55:21 +0000 |
commit | 81b527990c64a03a8b6942a7a0477e35ed144a76 (patch) | |
tree | 318511d4a32088789259218b0343ffe778586909 /kernel/mod_subst.ml | |
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 'kernel/mod_subst.ml')
0 files changed, 0 insertions, 0 deletions