aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-09 13:58:59 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:04 +0100
commit51976c9f2157953f794ed1efcd68403a8545d346 (patch)
tree612cc59179d2d16d5bb552f31f0abda92e50dd23 /kernel/univ.ml
parent6901f720c6115c8eec1343846641a5c8453c3268 (diff)
A bit of miscellaneous code documentation around notations.
Diffstat (limited to 'kernel/univ.ml')
0 files changed, 0 insertions, 0 deletions