aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-03-15 14:31:14 +0100
committerGaëtan Gilbert2019-04-25 15:20:36 +0200
commitb9c83781160edebc8a838b34e922578e709e2c66 (patch)
tree12b0253f099b1c8892b634bdccdd9362315d5df4 /doc/plugin_tutorial/tuto2/src
parent47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff)
inferCumulativity: shortcut for all-Invariant inductives
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src')
0 files changed, 0 insertions, 0 deletions