aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-12-16 17:23:33 +0100
committerMaxime Dénès2017-03-22 16:29:33 +0100
commitd2061bd8cd2d809d6e5a849dd150e9e0d74331fc (patch)
treeae840147edccf890fa3531487619adc87c2631c4 /kernel/nativecode.mli
parent8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff)
Remove duplicate lemmas.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions