aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtAtom.ml
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-6/+8
* | Use the Register mechanism (#104)ckeller2022-02-151-2/+2
* | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-141-1/+1
|\|
| * Small optimChantal Keller2021-10-141-1/+1
* | Merge remote-tracking branch 'smtcoq/master' into coq-8.10vblot2021-09-081-9/+12
|\|
| * generalize polymorphic arguments detectionvblot2021-09-081-9/+12
* | getting rid of native-coq (#95)vblot2021-05-281-25/+25
|/
* Update copyrightChantal Keller2021-05-261-1/+1
* Reify applied polymorphic terms with compdecChantal Keller2021-05-051-1/+7
* Solve a bug when reifying under a binderChantal Keller2021-04-281-2/+11
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-98/+172
* Reify polymorphic termsckeller2021-01-051-0/+15
* Empty bit-vectors are not valid in SMT (fixes #76)Chantal Keller2020-06-301-1/+1
* Failure instead of exception when atom is not well-typedChantal Keller2020-05-151-3/+1
* TypoChantal Keller2020-05-151-1/+0
* Close #10Chantal Keller2020-05-151-38/+55
* Solve bug in SMT printChantal Keller2020-05-151-17/+23
* V8.8 (#42)ckeller2019-03-111-16/+16
* V8.7 (#36)ckeller2019-02-141-22/+19
* equalities on array and bv types (#34)QGarchery2019-02-121-4/+4
* fix equality switch in lemmas (#27)QGarchery2019-01-301-5/+13
* Merge from LFSC (#26)ckeller2019-01-281-212/+931
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-84/+157
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-281-129/+16
* formattingQuentin Garchery2018-10-271-178/+178
* Updating of the copyrightChantal Keller2016-04-271-2/+3
* The tactic "verit" generates more user-friendly subgoalsChantal Keller2016-04-261-12/+13
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-10/+23
* Code refactoringChantal Keller2016-03-021-0/+13
* Identify ML functions that depend on native-coqChantal Keller2015-01-131-3/+3
* Initial import of SMTCoq v1.2Chantal Keller2015-01-121-0/+748
generated by cgit (git 2.34.1) at 2024-06-03 00:55:04 +0000