summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-06-17Coq: fix rich loop variablesBrian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
2020-01-21Reduce the amount of unnecessary parentheses in Coq outputBrian Campbell
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
2020-01-04Coq: change record field update notation to avoid duplicating termsBrian Campbell
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-10-28Coq: label fixpoint bodies, tweak spacingBrian Campbell
2019-10-25Coq: clean up some formattingBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-08-22additional option to tweak Coq output to support user-defined monad:pes20
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-16Fix all remaining tests for this branchAlasdair
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-20Coq: avoid more unnecessary uses of pattern bindersBrian Campbell
2019-06-20Coq: handle wildcard binders of bools properlyBrian Campbell
2019-06-13Add AST for greater-than and less-than constraintsBrian Campbell
2019-06-11Coq: improve readability of types filesBrian Campbell
2019-06-05Coq: fix type alias expansion in constraintsBrian Campbell
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-05-28Coq: don't output complex bool types at let expressionsBrian Campbell
2019-05-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-23Coq: support loops which update richly typed variablesBrian Campbell
2019-05-22Coq: replace inferrable integer arguments with _ at more typesBrian Campbell
2019-05-21Coq: introduce autocasts at variablesBrian Campbell
2019-05-20Coq: add some missing autocasts, avoid unnecessary patterns in letsBrian Campbell
2019-05-19Coq: remove unhelpful type printing restriction on early returnsBrian Campbell
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-04-19Coq: when replacing n_constraints in types allow for some rearrangementBrian Campbell
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
2019-04-16Coq: don't record assertions in the context if Sail doesn'tBrian Campbell
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-06Various bugfixes and improvementsAlasdair
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-04-05Coq: add missing effectful existential unpacking caseBrian Campbell
2019-04-04Coq: correct projection in plain monadic and/orBrian Campbell
2019-04-02Coq: replace n_constraints with equivalent bool variablesBrian Campbell
2019-03-21Coq: fix bug when multiple type variables map to the same identifierBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:09:40 +0000