aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-09 22:39:46 +0100
committerEmilio Jesus Gallego Arias2020-02-11 11:00:06 +0100
commitc9d76e9cd6953625778bf4b173430d674e15f05d (patch)
tree25646027db77bd8ff74d4faa315c070a60e61002 /kernel
parent4c6c173447d5b7d04aa0fd4f51d27a078c675708 (diff)
[coqdep] mli cleanup, remove unused functions
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions