Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Switch to 1.0 tag for traktitp22 | Chantal Keller | 2022-02-09 | 1 | -1/+1 |
| | |||||
* | Preparing release | Chantal Keller | 2022-02-09 | 1 | -1/+1 |
| | |||||
* | Merge remote-tracking branch 'origin/coq-8.13' into with-trakt | Chantal Keller | 2022-02-07 | 1 | -0/+32 |
|\ | |||||
| * | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2022-02-07 | 1 | -0/+32 |
| |\ | |||||
| | * | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2022-02-07 | 1 | -0/+32 |
| | |\ | |||||
| | | * | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2022-02-07 | 1 | -0/+32 |
| | | |\ | |||||
| | | | * | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2022-02-07 | 1 | -0/+32 |
| | | | |\ | |||||
| | | | | * | More silent simplifications from veriT | Chantal Keller | 2022-02-07 | 1 | -0/+32 |
| | | | | | | |||||
* | | | | | | Use the official repo for trakt | Chantal Keller | 2022-02-04 | 1 | -1/+1 |
| | | | | | | |||||
* | | | | | | All veriT tests go through | Chantal Keller | 2022-02-04 | 3 | -6/+73 |
| | | | | | | |||||
* | | | | | | Use trakt | Chantal Keller | 2022-02-04 | 7 | -951/+712 |
| | | | | | | |||||
* | | | | | | Temporarily switch to fork of trakt | Chantal Keller | 2022-02-04 | 1 | -2/+2 |
| | | | | | | |||||
* | | | | | | Local opam package | Chantal Keller | 2022-02-04 | 1 | -0/+44 |
|/ / / / / | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-12-07 | 4 | -5/+27 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-12-07 | 4 | -5/+27 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-12-07 | 4 | -5/+27 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-12-07 | 4 | -5/+27 |
| | | |\| | |||||
| | | | * | Solved bug in delayed ComDec | Chantal Keller | 2021-12-07 | 4 | -5/+27 |
| | | | | | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-11-15 | 2 | -1/+59 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-11-15 | 2 | -1/+59 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-11-15 | 2 | -1/+59 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-11-15 | 2 | -1/+59 |
| | | |\| | |||||
| | | | * | More bad instanciations by verit | Chantal Keller | 2021-11-15 | 2 | -1/+59 |
| | | | | | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-10-21 | 6 | -211/+134 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-10-21 | 6 | -211/+134 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-10-21 | 6 | -211/+134 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-10-21 | 6 | -211/+134 |
| | | |\| | |||||
| | | | * | Better use of the typeclass mechanism | Chantal Keller | 2021-10-21 | 6 | -210/+133 |
| | | | | | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-10-20 | 1 | -1/+68 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-10-20 | 1 | -1/+68 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-10-20 | 1 | -1/+68 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-10-20 | 1 | -1/+68 |
| | | |\| | |||||
| | | | * | prod is CompDec | Chantal Keller | 2021-10-20 | 1 | -1/+68 |
| | | | | | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-10-14 | 2 | -1/+44 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-10-14 | 2 | -1/+44 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-10-14 | 2 | -1/+44 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-10-14 | 2 | -1/+44 |
| | | |\| | |||||
| | | | * | Two examples showing that prenex dependency is handled, but not non-prenex one | Chantal Keller | 2021-10-14 | 1 | -0/+43 |
| | | | | | |||||
| | | | * | Small optim | Chantal Keller | 2021-10-14 | 1 | -1/+1 |
| | | | | | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-09-20 | 1 | -13/+2 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-09-20 | 1 | -13/+2 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-09-20 | 1 | -13/+2 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-09-20 | 1 | -13/+2 |
| | | |\| | |||||
| | | | * | Simplify apply_sym | Chantal Keller | 2021-09-20 | 1 | -13/+2 |
| | | | | | |||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-09-20 | 2 | -101/+67 |
|\| | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | Chantal Keller | 2021-09-20 | 2 | -101/+67 |
| |\| | | | |||||
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11 | Chantal Keller | 2021-09-20 | 2 | -101/+67 |
| | |\| | | |||||
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10 | Chantal Keller | 2021-09-20 | 2 | -101/+67 |
| | | |\| | |||||
| | | | * | vauto is now complete w.r.t. symmetry of equality (but may be exponential in ↵ | Chantal Keller | 2021-09-20 | 2 | -101/+67 |
| | | | | | | | | | | | | | | | | | | | | some cases) | ||||
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13 | Chantal Keller | 2021-09-17 | 2 | -1/+7 |
|\| | | | |