diff options
| author | Gaëtan Gilbert | 2020-02-12 14:05:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-13 15:12:48 +0100 |
| commit | bc2c1836ba4c878903288060bcb66a0ef1aaced6 (patch) | |
| tree | 1a340c43dedd24fd3db9a6063e8bbe449a32ca4a /kernel/cPrimitives.ml | |
| parent | bbf05cd2baa767c46ce95c1c185b87521afc0ec7 (diff) | |
Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)
Diffstat (limited to 'kernel/cPrimitives.ml')
0 files changed, 0 insertions, 0 deletions