aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 16:55:21 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 16:55:21 +0000
commit81b527990c64a03a8b6942a7a0477e35ed144a76 (patch)
tree318511d4a32088789259218b0343ffe778586909 /kernel/mod_subst.ml
parentef64634b31a4cd999cd08636adbf117f81889fb1 (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