summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
2018-07-02Coq: tidy up a bit of printingBrian Campbell
2018-07-02Coq: multiple record field updatesBrian Campbell
2018-07-02Work around Coq issue with pattern bindersBrian Campbell
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-22Coq: use simple forms for simple pattern matches in E_internal_letBrian Campbell
2018-06-20Coq: Generate MR when appropriate; syntax fixesBrian Campbell
2018-06-20Coq: add missing existential projection on simple let expressionsBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: print div/mod/abs in nexps; avoid mod as an identifierBrian Campbell
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-18Coq: better handling of identifiers, esp infix onesBrian Campbell
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
2018-06-12Coq: Handle simple top-level type variable definitionsBrian Campbell
2018-06-12Coq: upgrade some errors to report locationsBrian Campbell
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
2018-06-08Coq: some handling of existential types as function return typesBrian Campbell
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
2018-06-08Coq: track add_typquant changeBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
2018-06-08Coq: some very basic existential supportBrian Campbell
2018-06-08Coq: fix axiom generationBrian Campbell
2018-06-08Coq: update foreach handling, correct field accessesBrian Campbell
2018-06-08Coq: correct failure on unsupported undefined valuesBrian Campbell
2018-06-08Coq: use record update syntax (only single fields work for now)Brian Campbell
2018-06-08Coq: correct implicitness of type arguments in unionsBrian Campbell
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-28Coq: merge some implicit variables from axioms with argumentsBrian Campbell
2018-05-28Coq: prefer simple binders over patternsBrian Campbell
2018-05-28Coq: add option to produce axioms for unimplemented functionsBrian Campbell
2018-05-28Coq: proper printing of nexpsBrian Campbell
2018-05-24Coq: need None special case here, tooBrian Campbell
2018-05-24Coq: record conditionals in the context for constraint solvingBrian Campbell
2018-05-23Coq: Implement the most basic merging of type- and term-level parametersBrian Campbell
2018-05-04Rename type vars in Coq backend when they clash with identifiersBrian Campbell
2018-05-04Basic Coq constraintsBrian Campbell
2018-05-03Work in progress on the coq backendBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:13:03 +0000