summaryrefslogtreecommitdiff
path: root/lib/coq/Values.v
AgeCommit message (Expand)Author
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
2020-08-26Coq: replace a lot of omega with liaBrian Campbell
2020-08-26Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issueBrian Campbell
2020-08-26Coq: make some uses of auto in the library more robustBrian Campbell
2020-06-17Coq: implement shl_int_1Brian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell