sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2020-06-10	Prepare Coq library for packaging	Brian Campbell
	- rename files to get rid of prefix - use -Q to get package name right - add Base.v to make package imports simpler - add opam file for coq package
2019-11-29	Coq: switch to boolean predicates for Sail-type properties	Brian Campbell
	- ArithFact takes a boolean predicate - defined in terms of ArithFactP, which takes a Prop predicate, and is used directly for existentials - used abstract in more definitions with direct proofs - beef up solve_bool_with_Z to handle more equalities, andb and orb
2019-05-19	Coq: proper definitions for some undefined value functions	Brian Campbell
	That is, undefined_bitvector, undefined_unit, internal_pick.
2019-04-25	Update coq read_mem/write_mem.	Prashanth Mundkur

2019-04-10	Coq: update prompt monad to match the Lem, and port the state monad/lifting	Brian Campbell
	NB: requires minor changes in the models
2018-06-22	Coq: library updates, esp extending bitvector multiplies, Undefined	Brian Campbell

2018-06-19	Coq: library name update (as we did for Lem)	Brian Campbell