aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-1/+1
|\
| * CompDec on interpreted typeChantal Keller2021-05-051-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-052-2/+8
|\|
| * Reify applied polymorphic terms with compdecChantal Keller2021-05-052-2/+8
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-283-4/+18
|\|
| * Solve a bug when reifying under a binderChantal Keller2021-04-283-4/+18
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-1/+3
|\|
| * Take hypotheses from the local context (#91)ckeller2021-04-261-1/+3
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-211-15/+15
|\|
| * Solve a bound variable capture problem in the reification of quantified hypot...Chantal Keller2021-04-211-15/+15
* | Port to 8.10Chantal Keller2021-04-211-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-215-16/+57
|\|
| * Warning (instead of error) for unsupported lemmas (#90)ckeller2021-04-215-16/+57
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-213-2/+29
|\|
| * Convert hypotheses from Prop to bool (#89)ckeller2021-04-213-2/+29
* | Un-backport #87Chantal Keller2021-04-011-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-011-2/+3
|\|
| * Backport #87 to Coq-8.9 (closes #87)Chantal Keller2021-04-011-1/+1
| * use is_true from standard librarylduboisd2021-04-011-2/+3
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-02-236-165/+312
|\|
| * Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-236-165/+312
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-01-131-0/+15
|\|
| * Reify polymorphic termsckeller2021-01-051-0/+15
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-06-301-1/+1
|\|
| * Empty bit-vectors are not valid in SMT (fixes #76)Chantal Keller2020-06-301-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-05-152-57/+75
|\|
| * Failure instead of exception when atom is not well-typedChantal Keller2020-05-152-5/+1
| * TypoChantal Keller2020-05-151-1/+0
| * Close #10Chantal Keller2020-05-151-38/+55
| * Solve bug in SMT printChantal Keller2020-05-151-17/+23
* | Compiles with Coq-8.10Chantal Keller2020-03-311-1/+1
* | Port to coq-8.10 under progressChantal Keller2020-03-315-49/+48
|/
* Missing filesChantal Keller2019-09-252-0/+60
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-257-112/+80
* V8.9 (#43)ckeller2019-03-152-2/+2
* V8.8 (#42)ckeller2019-03-1116-588/+560
* V8.7 (#36)ckeller2019-02-149-163/+159
* equalities on array and bv types (#34)QGarchery2019-02-121-4/+4
* Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (has...QGarchery2019-02-071-13/+14
* fix equality switch in lemmas (#27)QGarchery2019-01-301-5/+13
* CleanupChantal Keller2019-01-292-2/+2
* Merge from LFSC (#26)ckeller2019-01-2820-883/+3191
* verit also works when it doesn't use the conclusion (#24)QGarchery2018-12-033-2/+34
* Adding support for lemmas in the command veritQuentin Garchery2018-10-2818-211/+570
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-286-179/+158
* formattingQuentin Garchery2018-10-278-509/+497
* Zeq_bool -> Z.eqbQuentin Garchery2018-10-271-4/+1
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-201-2/+2
* - auto-generated mli files for future documentationValentin Blot2017-11-247-0/+471
* Command to bypass typechecking when generating a zchaff theoremChantal Keller2017-11-141-0/+3
generated by cgit (git 2.34.1) at 2024-06-13 09:44:33 +0000