aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
* | | | | 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-201-101/+30
|\| | | |
| * | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-09-201-101/+30
| |\| | |
| | * | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-09-201-101/+30
| | |\| |
| | | * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-201-101/+30
| | | |\|
| | | | * vauto is now complete w.r.t. symmetry of equality (but may be exponential in ...Chantal Keller2021-09-201-101/+30
* | | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-171-1/+1
|\| | | |
| * | | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-09-171-1/+1
| |\| | |
| | * | | Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11Chantal Keller2021-09-171-1/+1
| | |\| |
| | | * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-171-1/+1
| | | |\|
| | | | * Solve bug in prop2boolChantal Keller2021-09-171-1/+1
* | | | | 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
| | | |\|
| | | | * generalize polymorphic arguments detectionvblot2021-09-081-9/+12
* | | | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-08-303-3/+3
|\| | | |
| * | | | Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12Chantal Keller2021-08-303-3/+3
| |\| | |
| | * | | Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11Chantal Keller2021-08-303-3/+3
| | |\| |
| | | * | Rename directory because MacOS FS is case-insensitiveChantal Keller2021-08-303-3/+3
* | | | | Merge remote-tracking branch 'origin/coq-8.12' into HEADvblot2021-08-252-1/+3
|\| | | |
| * | | | Merge remote-tracking branch 'origin/coq-8.11' into HEADvblot2021-08-252-1/+3
| |\| | |
| | * | | Merge remote-tracking branch 'origin/coq-8.10' into HEADvblot2021-08-252-1/+3
| | |\| |
| | | * | Merge remote-tracking branch 'origin/master' into HEADvblot2021-08-252-1/+3
| | | |\|
| | | | * fix array notations clash with ssreflectvblot2021-08-252-1/+3
* | | | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-07-111-58/+63
|\| | | |
| * | | | Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12Chantal Keller2021-07-111-58/+63
| |\| | |
| | * | | Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11Chantal Keller2021-07-111-58/+63
| | |\| |
| | | * | Merge remote-tracking branch 'remotes/origin/master' into coq-8.10Chantal Keller2021-07-111-58/+63
| | | |\|
| | | | * The verit tactics now immediately fail if veriT is not installedChantal Keller2021-07-111-58/+63
* | | | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-07-0726-5056/+1688
|\| | | |
| * | | | Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12Chantal Keller2021-07-0726-5036/+1668
| |\| | |
| | * | | Ring must be importedChantal Keller2021-07-071-1/+1
| | * | | Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11Chantal Keller2021-07-0725-5042/+1664
| | |\| |
| | | * | use native integers (#96)vblot2021-07-0725-5042/+1664
* | | | | All tests go throughChantal Keller2021-06-071-1/+1
* | | | | Lia + factorize codeChantal Keller2021-06-075-130/+97
* | | | | Remove new warningChantal Keller2021-06-071-4/+4
* | | | | Port the Coq partChantal Keller2021-06-074-20/+26
* | | | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-06-075-36/+983
|\| | | |
| * | | | Configure not needed anymoreChantal Keller2021-06-072-4/+866
| * | | | Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12Chantal Keller2021-06-073-32/+117
| |\| | |
| | * | | Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11Chantal Keller2021-06-023-32/+117
| | |\| |
| | | * | Merge remote-tracking branch 'remotes/origin/master' into coq-8.10Chantal Keller2021-06-023-32/+117
| | | |\|
| | | | * Type back in CompDec (for efficiency reasons)Chantal Keller2021-06-023-32/+117
* | | | | Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13Chantal Keller2021-05-282-866/+4
|\| | | |