aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-11-04 18:00:18 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-11-05 10:08:20 +0100
commitd8baa76d86eaa691a5386669596a6004bb44bb7a (patch)
treec7008e731003ab9bef4ece94c7d85738fe402ad9 /kernel/names.ml
parentdc4200a1c0e37a600537fd1809377a3137ce0cc3 (diff)
More precise refine compatibility
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions