sail/lib/coq, branch sail2 Formal specification language for ISAs Tweak Coq proof to avoid incompatibility with Iris 2020-09-30T16:26:09+00:00 Brian Campbell 2020-09-30T16:25:56+00:00 ce94aec9d6604b41217529525b7a73850c530e7b (in the previous proof script the intuition tactic found a strange proof involving a type-level dependent pair that imposed an unnecessary universe constraint, this doesn't) 
(in the previous proof script the intuition tactic found a strange proof
involving a type-level dependent pair that imposed an unnecessary
universe constraint, this doesn't)
Merge some of the gitignore files 2020-09-12T21:00:19+00:00 Columbus240 2020-08-24T17:27:33+00:00 a8be1e2551bc4fbda9c45792c0dad5743c18fefd Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq. This commit removes /lib/coq/.gitignore and moves all ignore-statements to /.gitignore . This should simplify the maintenance of gitignore files. The situation with /test/mono/.gitignore is analogous. 
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.

The situation with /test/mono/.gitignore is analogous.
Coq: replace other uses of omega with lia 2020-08-26T09:34:58+00:00 Brian Campbell 2020-08-25T21:52:07+00:00 0859ca09e733f900ec866f129d823f754a6acbae Also remove omega workaround that lia doesn't need. 
Also remove omega workaround that lia doesn't need.
Coq: replace a lot of omega with lia 2020-08-26T09:34:57+00:00 Brian Campbell 2020-08-25T20:42:26+00:00 9c6d3c66ca9cd8f328ae1c37caf1b65a2bbba448 






Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issue
2020-08-26T09:34:57+00:00

Brian Campbell

2020-08-25T17:36:19+00:00

ce87c17955727a7c2a0178a635c4bd17edd4252c












Coq: make some uses of auto in the library more robust
2020-08-26T09:34:57+00:00

Brian Campbell

2020-08-25T17:32:15+00:00

ac2d2a9e0115693064d10d38ad8208a0e9f70b43












Coq: implement shl_int_1
2020-06-17T20:14:09+00:00

Brian Campbell

2020-06-17T20:14:09+00:00

2e8928231f46e5f0cfb454849dd41731a3201867












Coq: tidy up scope in library
2020-06-14T22:18:34+00:00

Brian Campbell

2020-06-14T21:27:30+00:00

e22bb9841a5186d0b52b8fa9ad8cf2e46fa51d76

Helps with Coq 8.11.  Also fix BBVDIR default in test script.





Helps with Coq 8.11.  Also fix BBVDIR default in test script.







Coq: fix matching bug in solver
2020-06-12T17:56:19+00:00

Brian Campbell

2020-06-12T17:40:42+00:00

b6fb5a567c1d3d0bbe1f30e875d2cdcaba9514ad












Coq: specialise the andor solvers to avoid excessive search and solve more goals
2020-06-11T16:22:26+00:00

Brian Campbell

2020-06-11T16:22:26+00:00

9468ad12ea50d5fcafda669706b65005820a3ba9