aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorJason Gross2016-12-12 16:37:03 -0500
committerMaxime Dénès2016-12-19 08:51:35 +0100
commita56e966162aee59b6044c1fd1d9d4e43c33eba35 (patch)
treeeccf53c5437280c2b8b96f9b2a53dd5e52c572ec /kernel/nativecode.ml
parentfe4a29ef11c2db8ffb26ef0ba0775fc939471ac9 (diff)
Fix a typo in Hurkens.v comment
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions