aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-02-14 15:12:19 +0100
committerGaëtan Gilbert2019-02-18 21:24:10 +0100
commit7cb49eda2c33c620f020cf7487ab9f53b74859da (patch)
tree6680f9380932fd53e3198518aa28063871fe4835 /kernel
parenteb20b899a6cd0e3b9816a4b6824998255c4af6b8 (diff)
Sphinx: remove [coqtop:: undo]
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions