summaryrefslogtreecommitdiff
path: root/test/coq
AgeCommit message (Expand)Author
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