summaryrefslogtreecommitdiff
path: root/test/coq
AgeCommit message (Expand)Author
2020-09-25tests: Move copy-pasted code into a shared helper .shAlex Richardson
2020-06-14Coq: tidy up scope in libraryBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-09-02Enable part of a test that's been fixed recently.Brian Campbell
2019-08-30Add a couple of overlooked testsBrian Campbell
2019-06-21Coq: add missing property derivation casts for effectful expressionsBrian Campbell
2019-06-21Coq: be more careful when dealing with wildcard argument patternsBrian Campbell
2019-06-03Test case for previous commitBrian Campbell
2019-05-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-21Coq: introduce autocasts at variablesBrian Campbell
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-05Coq: add missing effectful existential unpacking caseBrian Campbell
2019-04-04Coq: improve solver on conjunctions, Euclidean division/moduloBrian Campbell
2019-04-02Coq: replace n_constraints with equivalent bool variablesBrian Campbell
2019-03-20Coq: be more careful about merging Sail variables and type variablesBrian Campbell
2019-03-19Coq: more test workBrian Campbell
2019-03-19Coq: more work on testsBrian Campbell
2019-03-15Coq: some progress on the test suiteBrian Campbell
2019-03-15Add coq test case for for-loop type variableBrian Campbell
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian Campbell
2018-10-12Prevent accidental test failures when Coq compiles in the wrong orderBrian Campbell
2018-07-27Coq: patterns on bit literalsBrian Campbell
2018-07-23Coq test for a few non-trivial atom typesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-06-26In guarded pattern rewriting, irrefutable patterns subsume wildcardsBrian Campbell
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Coq: ignore some currently unsupported testsBrian Campbell
2018-06-08Coq: skip two tests with redundant pattern matchesBrian Campbell
2018-05-28Coq: add back tests with undefined functionsBrian Campbell
2018-05-28Coq: add option to produce axioms for unimplemented functionsBrian Campbell
2018-05-24Import (rather hacky) Coq Sail librariesBrian Campbell
2018-05-03Work in progress on the coq backendBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:12:47 +0000