aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-12-074-5/+27
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-12-074-5/+27
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-12-074-5/+27
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-12-074-5/+27
| | | |\| |
| | | | * | Solved bug in delayed ComDecChantal Keller2021-12-074-5/+27
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-11-152-1/+59
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-11-152-1/+59
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-11-152-1/+59
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-11-152-1/+59
| | | |\| |
| | | | * | More bad instanciations by veritChantal Keller2021-11-152-1/+59
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-10-216-211/+134
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-10-216-211/+134
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-10-216-211/+134
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-216-211/+134
| | | |\| |
| | | | * | Better use of the typeclass mechanismChantal Keller2021-10-216-210/+133
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-10-201-1/+68
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-10-201-1/+68
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-10-201-1/+68
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-201-1/+68
| | | |\| |
| | | | * | prod is CompDecChantal Keller2021-10-201-1/+68
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-10-142-1/+44
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-10-142-1/+44
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-10-142-1/+44
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-142-1/+44
| | | |\| |
| | | | * | Two examples showing that prenex dependency is handled, but not non-prenex oneChantal Keller2021-10-141-0/+43
| | | | * | Small optimChantal Keller2021-10-141-1/+1
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-201-13/+2
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-09-201-13/+2
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-09-201-13/+2
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-201-13/+2
| | | |\| |
| | | | * | Simplify apply_symChantal Keller2021-09-201-13/+2
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-202-101/+67
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-09-202-101/+67
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-09-202-101/+67
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-202-101/+67
| | | |\| |
| | | | * | vauto is now complete w.r.t. symmetry of equality (but may be exponential in ...Chantal Keller2021-09-202-101/+67
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-172-1/+7
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-09-172-1/+7
| |\| | | |
| | * | | | Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11Chantal Keller2021-09-172-1/+7
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-172-1/+7
| | | |\| |
| | | | * | Solve bug in prop2boolChantal Keller2021-09-172-1/+7
* | | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-161-0/+2
|\| | | | |
| * | | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-09-161-0/+2
| |\| | | |
| | * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-09-161-0/+2
| | |\| | |
| | | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-161-0/+2
| | | |\| |
| | | | * | Update the list of authors and institutesChantal Keller2021-09-161-0/+2
* | | | | | Merge remote-tracking branch 'coq-8.12' into coq-8.13vblot2021-09-081-9/+12
|\| | | | |
| * | | | | Merge remote-tracking branch 'coq-8.11' into coq-8.12vblot2021-09-081-9/+12
| |\| | | |
| | * | | | Merge remote-tracking branch 'coq-8.10' into coq-8.11vblot2021-09-081-9/+12
| | |\| | |
| | | * | | Merge remote-tracking branch 'smtcoq/master' into coq-8.10vblot2021-09-081-9/+12
| | | |\| |