aboutsummaryrefslogtreecommitdiff
path: root/dev
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 /dev
parent47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff)
inferCumulativity: shortcut for all-Invariant inductives
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions