aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Remove unused record fieldSMTCoq-2.0+8.11Chantal Keller2022-05-041-2/+1
* Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-05-041-24/+24
|\
| * Merge remote-tracking branch 'origin/coq-8.9' into coq-8.10Chantal Keller2022-05-041-24/+24
| |\
| | * Comment testsChantal Keller2022-05-041-24/+24
* | | Clean-upChantal Keller2022-04-145-14/+84
* | | PortChantal Keller2022-04-141-42/+45
* | | Merge remote-tracking branch 'origin/coq-8.11' into timeout_veritChantal Keller2022-04-14126-6243/+3631
|\ \ \
| * | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-02-181-19/+255
| |\| |
| | * | Merge remote-tracking branch 'vblot/coq-8.10-foldi_iter' into coq-8.10Chantal Keller2022-02-181-19/+254
| | |\ \
| | | * | simpler foldi_itervblot2022-02-181-42/+251
| | | * | foldi_itervblot2022-02-151-13/+39
| * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-02-172-1/+5
| |\| | |
| | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-172-1/+5
| | |\ \ \ | | | | |/ | | | |/|
| | | * | Improve make cleanallChantal Keller2022-02-172-1/+5
| * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-02-17115-135/+137
| |\| | |
| | * | | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-17115-115/+115
| | |\| |
| | | * | Update copyrightChantal Keller2022-02-16126-126/+126
| | * | | Add debugging information for uninterpreted functionsChantal Keller2022-02-166-20/+22
| * | | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-02-1519-585/+983
| |\| | |
| | * | | Use the Register mechanism (#104)ckeller2022-02-1519-585/+983
| | | |/ | | |/|
| * | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-02-071-0/+32
| |\| |
| | * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-071-0/+32
| | |\|
| | | * More silent simplifications from veriTChantal Keller2022-02-071-0/+32
| * | | 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.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.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.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.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.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.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 '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.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
| | |\|