aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-12 14:05:53 +0100
committerGaëtan Gilbert2020-02-13 15:12:48 +0100
commitbc2c1836ba4c878903288060bcb66a0ef1aaced6 (patch)
tree1a340c43dedd24fd3db9a6063e8bbe449a32ca4a /kernel/cbytecodes.mli
parentbbf05cd2baa767c46ce95c1c185b87521afc0ec7 (diff)
Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions