aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorJason Gross2017-06-11 20:22:43 -0400
committerGitHub2017-06-11 20:22:43 -0400
commit75f42c5c4f350f301ef1968459f4f19f7a349ad4 (patch)
tree272ca2e26030fe1d4e487c68db3b0444ef4de29d /kernel/nativecode.ml
parent79c42e22dd5106dcb85229ceec75331029ab5486 (diff)
Point ci-hott at a newer version of HoTT
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions