aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-18 18:58:21 +0100
committerMaxime Dénès2017-12-18 18:58:21 +0100
commit9266d34a073859f24aa615767a1311d532bba0ac (patch)
treecda62961092f0162a5ce950a9a6b70ab4a5cd4b2 /kernel/nativecode.mli
parent7e2f9861f3d38829baf246883e4925d48c9e2998 (diff)
parent4024286d9fdd13e5ec4c474b1dae4ce58ac41683 (diff)
Merge PR #6381: A version of [time] that works on constr evaluation
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions