sail/test/coq, branch sail2 Formal specification language for ISAs tests: Move copy-pasted code into a shared helper .sh 2020-09-25T11:30:09+00:00 Alex Richardson 2020-09-25T09:12:56+00:00 782d3860eb0134c81d4a4204b7caab72cda3bd1d Also fix a few shellcheck warnings related to printf while doing so. 
Also fix a few shellcheck warnings related to printf while doing so.
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.
Prepare Coq library for packaging 2020-06-10T20:38:06+00:00 Brian Campbell 2020-06-10T20:33:09+00:00 d2b4a7a1d654cf8f315e2471b1470506255f3d68 - 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 
- 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
Update path for newer versions of BBV Coq library 2020-04-10T12:22:11+00:00 Thomas Bauereiss 2020-03-27T18:06:26+00:00 550db27f8c27e03ecc4defc804c8f360af64fbd6 






Coq: remove last use and definition of doc_nc_prop
2019-12-01T21:34:23+00:00

Brian Campbell

2019-12-01T21:34:23+00:00

92db256a63619b46f3b46169a45205de4f840de7

(plus test, as it wasn't covered before)





(plus test, as it wasn't covered before)







Coq: limited support for existentially-typed tuples
2019-10-02T10:40:38+00:00

Brian Campbell

2019-10-02T10:40:38+00:00

2d1051cc4a1dfdd1a55e2df6ba331d7f1954bb61

- in particular at monadic interfaces (i.e., sufficient for instruction
  ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
  example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)





- in particular at monadic interfaces (i.e., sufficient for instruction
  ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
  example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)







Enable part of a test that's been fixed recently.
2019-09-02T16:04:09+00:00

Brian Campbell

2019-09-02T16:04:09+00:00

78ff67666473029726ed1b62fdbc6edc7d1d8812












Add a couple of overlooked tests
2019-08-30T13:38:29+00:00

Brian Campbell

2019-08-30T13:38:29+00:00

767c50a4ba8661b657dd5142fd7ae491eb52ddb6












Coq: add missing property derivation casts for effectful expressions
2019-06-21T13:44:29+00:00

Brian Campbell

2019-06-21T13:44:29+00:00

e8697cb036720cdf75687f0c442c49dd48913bcb

These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.





These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.







Coq: be more careful when dealing with wildcard argument patterns
2019-06-21T09:57:15+00:00

Brian Campbell

2019-06-21T09:57:15+00:00

7a5f75524c59bf885d7c31ed1ae8a7cfe725d5dc

If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.





If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.