aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests
Commit message (Expand)AuthorAgeFilesLines
* New case for vautoChantal Keller2022-07-291-0/+27
* Do not add CompDec on the flyChantal Keller2022-05-061-0/+19
* Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2022-04-141-0/+64
|\
| * Clean-upChantal Keller2022-04-141-0/+64
* | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2022-02-171-1/+1
|\|
| * 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
| |/|
| | * Improve make cleanallChantal Keller2022-02-171-1/+1
* | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2022-02-177-7/+7
|\| |
| * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-177-7/+7
| |\|
| | * Update copyrightChantal Keller2022-02-167-7/+7
* | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-12-071-0/+23
|\| |
| * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-12-071-0/+23
| |\|
| | * Solved bug in delayed ComDecChantal Keller2021-12-071-0/+23
* | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-11-151-0/+26
|\| |
| * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-11-151-0/+26
| |\|
| | * More bad instanciations by veritChantal Keller2021-11-151-0/+26
* | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-10-141-0/+43
|\| |
| * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-141-0/+43
| |\|
| | * Two examples showing that prenex dependency is handled, but not non-prenex oneChantal Keller2021-10-141-0/+43
* | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-201-0/+37
|\| |
| * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-201-0/+37
| |\|
| | * vauto is now complete w.r.t. symmetry of equality (but may be exponential in ...Chantal Keller2021-09-201-0/+37
* | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-09-171-0/+6
|\| |
| * | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-09-171-0/+6
| |\|
| | * Solve bug in prop2boolChantal Keller2021-09-171-0/+6
* | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-07-071-7/+7
|/ /
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-267-7/+7
|\|
| * Update copyrightChantal Keller2021-05-267-7/+7
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-061-0/+22
|\|
| * Another silent change of veriT...Chantal Keller2021-05-061-0/+22
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-061-0/+12
|\|
| * Example for #92Chantal Keller2021-05-061-0/+12
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-0/+35
|\|
| * CompDec on interpreted typeChantal Keller2021-05-051-0/+35
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-0/+31
|\|
| * Reify applied polymorphic terms with compdecChantal Keller2021-05-051-0/+31
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-281-0/+14
|\|
| * Solve a bug when reifying under a binderChantal Keller2021-04-281-0/+14
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-0/+11
|\|
| * Equality between Booleans should be changed for hypothesesChantal Keller2021-04-261-0/+11
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-4/+13
|\|
| * CompDec are automatically discharged when generated by the OCaml tactic, when...Chantal Keller2021-04-261-4/+13
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-262-57/+51
|\|
| * Take hypotheses from the local context (#91)ckeller2021-04-262-57/+51
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-212-40/+173
|\|
| * Convert hypotheses from Prop to bool (#89)ckeller2021-04-212-40/+173
* | Batch parallelismChantal Keller2021-02-231-1/+1
|/
* Example of groups in unit testsChantal Keller2021-02-231-18/+37
* The examples on lists uses the true list typeChantal Keller2021-02-231-10/+5
generated by cgit (git 2.34.1) at 2024-05-05 15:49:27 +0000