aboutsummaryrefslogtreecommitdiffstats
path: root/src/PropToBool.v
Commit message (Expand)AuthorAgeFilesLines
* Do not add CompDec on the flyChantal Keller2022-05-061-187/+256
* 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
* | | Merge remote-tracking branch 'origin/coq-8.11' into timeout_veritChantal Keller2022-04-141-5/+5
|\ \ \
| * | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2022-02-171-1/+1
| |\| |
| | * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-171-1/+1
| | |\|
| | | * Update copyrightChantal Keller2022-02-161-1/+1
| * | | Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11Chantal Keller2021-10-211-3/+3
| |\| |
| | * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-211-3/+3
| | |\|
| | | * Better use of the typeclass mechanismChantal Keller2021-10-211-3/+3
| * | | 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
* | | | use of anomaly for timeoutlduboisd2022-04-081-5/+5
|/ / /
* | | Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11Chantal Keller2021-05-261-1/+1
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-261-1/+1
| |\|
| | * Update copyrightChantal Keller2021-05-261-1/+1
* | | Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11Chantal Keller2021-05-051-1/+0
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-1/+0
| |\|
| | * CompDec on interpreted typeChantal Keller2021-05-051-1/+0
* | | Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11Chantal Keller2021-05-051-1/+24
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-1/+24
| |\|
| | * Reify applied polymorphic terms with compdecChantal Keller2021-05-051-1/+24
* | | Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11Chantal Keller2021-04-281-2/+2
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-281-2/+2
| |\|
| | * prop2bool_hyps insensitive to parenthesisChantal Keller2021-04-281-2/+2
* | | Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11Chantal Keller2021-04-261-3/+11
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-3/+11
| |\|
| | * Equality between Booleans should be changed for hypothesesChantal Keller2021-04-261-3/+11
* | | Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11Chantal Keller2021-04-261-3/+10
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-3/+10
| |\|
| | * Take hypotheses from the local context (#91)ckeller2021-04-261-3/+10
* | | Port to 8.11Chantal Keller2021-04-211-2/+2
|/ /
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-211-4/+246
|\|
| * Convert hypotheses from Prop to bool (#89)ckeller2021-04-211-4/+246
|/
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-25/+23
* Merge from LFSC (#26)ckeller2019-01-281-0/+85