summaryrefslogtreecommitdiff
path: root/mips/mips_extras.v
AgeCommit message (Expand)Author
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-02Coq mips: fix deprecation warningBrian Campbell
2018-08-02Coq: remove type removal holdover from Lem backend, add MIPS lemmaBrian Campbell
2018-07-23Coq: faster MIPS extras without confusing messageBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-03Fill in a few Coq functions for CHERI from the MIPS preludeBrian Campbell
2018-07-02Coq modulus operation that fits the typeBrian Campbell
2018-06-22Add current state of mips_extras.vBrian Campbell