| Age | Commit message (Expand) | Author |
|---|
| 2018-07-09 | Coq: remove some unnecessary casts | Brian Campbell |
| 2018-07-07 | Coq: precise generic vectors | Brian Campbell |
| 2018-07-07 | Coq: supply index constraint in for loops | Brian Campbell |
| 2018-07-06 | Coq: support assertions inside and outside of blocks | Brian Campbell |
| 2018-07-06 | Coq: avoid nexp simplification when deciding whether a cast is needed | Brian Campbell |
| 2018-07-06 | Coq: Avoid clashes with the monad name, M | Brian Campbell |
| 2018-07-06 | Coq: feed assertions into the context | Brian Campbell |
| 2018-07-06 | Coq: reduce use of sumbool_of_bool to relevant constraints | Brian Campbell |
| 2018-07-06 | Coq: missing existential building for ranges | Brian Campbell |
| 2018-07-06 | Coq: turn off partial support for dropping true constraints, fix strings | Brian Campbell |
| 2018-07-02 | Coq: tidy up a bit of printing | Brian Campbell |
| 2018-07-02 | Coq: multiple record field updates | Brian Campbell |
| 2018-07-02 | Work around Coq issue with pattern binders | Brian Campbell |
| 2018-06-25 | Coq: add typeclass based comparison, and instantiate for enums | Brian Campbell |
| 2018-06-25 | Coq: automatic cast introduction | Brian Campbell |
| 2018-06-22 | Coq: use simple forms for simple pattern matches in E_internal_let | Brian Campbell |
| 2018-06-20 | Coq: Generate MR when appropriate; syntax fixes | Brian Campbell |
| 2018-06-20 | Coq: add missing existential projection on simple let expressions | Brian Campbell |
| 2018-06-20 | Coq: Tidy up libraries, export String | Brian Campbell |
| 2018-06-20 | Coq: print div/mod/abs in nexps; avoid mod as an identifier | Brian Campbell |
| 2018-06-20 | Coq: port handling of effectful and/or from Lem backend | Brian Campbell |
| 2018-06-18 | Coq: better handling of identifiers, esp infix ones | Brian Campbell |
| 2018-06-13 | Coq: library updates, informative type errors, fix type aliases | Brian Campbell |
| 2018-06-12 | Coq: Handle simple top-level type variable definitions | Brian Campbell |
| 2018-06-12 | Coq: upgrade some errors to report locations | Brian Campbell |
| 2018-06-12 | Coq: support for range type, along with related existential improvements | Brian Campbell |
| 2018-06-08 | Coq: some handling of existential types as function return types | Brian Campbell |
| 2018-06-08 | Coq: add destructuring of atom existentials in patterns | Brian Campbell |
| 2018-06-08 | Coq: track add_typquant change | Brian Campbell |
| 2018-06-08 | Coq: existential and constraint solving work | Brian Campbell |
| 2018-06-08 | Coq: some very basic existential support | Brian Campbell |
| 2018-06-08 | Coq: fix axiom generation | Brian Campbell |
| 2018-06-08 | Coq: update foreach handling, correct field accesses | Brian Campbell |
| 2018-06-08 | Coq: correct failure on unsupported undefined values | Brian Campbell |
| 2018-06-08 | Coq: use record update syntax (only single fields work for now) | Brian Campbell |
| 2018-06-08 | Coq: correct implicitness of type arguments in unions | Brian Campbell |
| 2018-06-06 | Some work on improving error messages | Alasdair Armstrong |
| 2018-05-28 | Coq: merge some implicit variables from axioms with arguments | Brian Campbell |
| 2018-05-28 | Coq: prefer simple binders over patterns | Brian Campbell |
| 2018-05-28 | Coq: add option to produce axioms for unimplemented functions | Brian Campbell |
| 2018-05-28 | Coq: proper printing of nexps | Brian Campbell |
| 2018-05-24 | Coq: need None special case here, too | Brian Campbell |
| 2018-05-24 | Coq: record conditionals in the context for constraint solving | Brian Campbell |
| 2018-05-23 | Coq: Implement the most basic merging of type- and term-level parameters | Brian Campbell |
| 2018-05-04 | Rename type vars in Coq backend when they clash with identifiers | Brian Campbell |
| 2018-05-04 | Basic Coq constraints | Brian Campbell |
| 2018-05-03 | Work in progress on the coq backend | Brian Campbell |
