| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-16 | Add the type an expression was checked against to tannots, and use for Coq | Brian Campbell | |
| Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast. | |||
| 2018-08-15 | Get RISC-V on Coq into reasonable state to show | Brian Campbell | |
| - 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 | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |