summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
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