sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-06-12	Coq: support for range type, along with related existential improvements	Brian Campbell
	Plus - Complete solver support for inequalities - Reduce exponentials in solver
2018-06-08	Coq: add destructuring of atom existentials in patterns	Brian Campbell
	Plus test case, broken builtin name
2018-06-08	Coq: ignore some currently unsupported tests	Brian Campbell

2018-06-08	Coq: skip two tests with redundant pattern matches	Brian Campbell

2018-05-28	Coq: add back tests with undefined functions	Brian Campbell

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