summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorBrian Campbell2018-08-15 13:59:16 +0100
committerBrian Campbell2018-08-15 13:59:16 +0100
commitb73f6d13b4bf2291f71616abdb046e2ca657d868 (patch)
treee999f8ccde5f510a9c004197b7fa142c346d9982 /src/process_file.ml
parent39fea17bac77535c9cff47cd6657a308e391ac8a (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 'src/process_file.ml')
0 files changed, 0 insertions, 0 deletions