aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtForm.ml
Commit message (Expand)AuthorAgeFilesLines
* Update copyrightChantal Keller2022-02-161-1/+1
* Update copyrightChantal Keller2021-05-261-1/+1
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-2/+2
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-251-20/+40
* V8.8 (#42)ckeller2019-03-111-15/+15
* V8.7 (#36)ckeller2019-02-141-1/+1
* Merge from LFSC (#26)ckeller2019-01-281-172/+265
* verit also works when it doesn't use the conclusion (#24)QGarchery2018-12-031-1/+3
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-26/+63
* formattingQuentin Garchery2018-10-271-249/+241
* Compiles with Coq-8.6Chantal Keller2017-10-031-7/+6
* Updating of the copyrightChantal Keller2016-04-271-2/+4
* Compatibility with native-coqChantal Keller2016-04-261-6/+6
* Tactic zchaff for 8.5Chantal Keller2016-04-261-7/+14
* Identify ML functions that depend on native-coqChantal Keller2015-01-131-2/+2
* Initial import of SMTCoq v1.2Chantal Keller2015-01-121-0/+510