aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtAtom.mli
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-171-1/+1
|\
| * Update copyrightChantal Keller2022-02-161-1/+1
* | Add debugging information for uninterpreted functionsChantal Keller2022-02-161-1/+1
* | getting rid of native-coq (#95)vblot2021-05-281-13/+13
|/
* 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