| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-12 | Prevent accidental test failures when Coq compiles in the wrong order | Brian Campbell | |
| 2018-07-07 | Coq: bbv have reorganised their repository | Brian Campbell | |
| 2018-06-08 | Coq: add destructuring of atom existentials in patterns | Brian Campbell | |
| Plus test case, broken builtin name | |||
| 2018-05-28 | Coq: add option to produce axioms for unimplemented functions | Brian Campbell | |
| Useful for partial test cases (e.g., some of the typechecking tests) Also a bonus warning for such functions in normal use | |||
| 2018-05-24 | Import (rather hacky) Coq Sail libraries | Brian Campbell | |
| 2018-05-03 | Work in progress on the coq backend | Brian Campbell | |
| - originally based on the Lem backend - added externs to some of the library files and tests - added wildcard to extern valspecs in parser - added Type_check.get_val_spec_orig to return the valspec with the function's original names for bound type variables Note that most of the tests will fail currently | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |