aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtAtom.mli
Commit message (Expand)AuthorAgeFilesLines
* Update copyrightChantal Keller2021-05-261-1/+1
* Solve a bug when reifying under a binderChantal Keller2021-04-281-0/+1
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-2/+2
* Failure instead of exception when atom is not well-typedChantal Keller2020-05-151-2/+0
* V8.8 (#42)ckeller2019-03-111-13/+13
* Merge from LFSC (#26)ckeller2019-01-281-52/+96
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-14/+31
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-281-40/+3
* formattingQuentin Garchery2018-10-271-2/+3
* Updating of the copyrightChantal Keller2016-04-271-2/+2
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-0/+2
* Code refactoringChantal Keller2016-03-021-0/+4
* Initial import of SMTCoq v1.2Chantal Keller2015-01-121-0/+175