diff options
| author | Gaëtan Gilbert | 2020-02-14 10:53:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-17 13:22:15 +0100 |
| commit | 4165cce72347466fbaa565247ae040a873b46694 (patch) | |
| tree | 05f22b076d46384a3672c06a98731c7cf1af37b2 /kernel/nativecode.mli | |
| parent | d122f7d5ffd5d3b26153a0ad7b74a669b8dd1c9d (diff) | |
Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions