diff options
| author | Brian Campbell | 2018-08-15 13:59:16 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-15 13:59:16 +0100 |
| commit | b73f6d13b4bf2291f71616abdb046e2ca657d868 (patch) | |
| tree | e999f8ccde5f510a9c004197b7fa142c346d9982 /riscv/platform.ml | |
| parent | 39fea17bac77535c9cff47cd6657a308e391ac8a (diff) | |
Get RISC-V on Coq into reasonable state to show
- Fill in Coq builtins for more of the RISC-V prelude
- Update Barriers
- More general autocast
- Temporary sub_nat definition (until the backend handles nat better)
- Patch to bring results into a reasonable state
- Use Let rather than Definition for non-dependent top-level values
Diffstat (limited to 'riscv/platform.ml')
0 files changed, 0 insertions, 0 deletions