aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests
Commit message (Expand)AuthorAgeFilesLines
* Clean-upChantal Keller2022-04-141-0/+64
* 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/master' into coq-8.10Chantal Keller2022-02-177-7/+7
|\|
| * Update copyrightChantal Keller2022-02-167-7/+7
* | 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/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/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/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/master' into coq-8.10Chantal Keller2021-09-171-0/+6
|\|
| * Solve bug in prop2boolChantal Keller2021-09-171-0/+6
* | 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
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-232-27/+218
* Reify polymorphic termsckeller2021-01-051-0/+10
* Testing BV subtractionChantal Keller2020-07-201-0/+16
* Close #10Chantal Keller2020-05-151-0/+18
* Test asynchronous and make the selected lemmas persistant (#66)ckeller2020-03-264-202/+246
* make test does not need cleaning anymoreChantal Keller2020-03-251-2/+6
* Add the full example of the webpage in the unit testsChantal Keller2020-01-161-0/+30
* Separate unit tests into vernac and tacticsChantal Keller2019-04-126-533/+580
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-121-1/+1
* V8.7 (#36)ckeller2019-02-142-40/+16
* Cleaning (#35)QGarchery2019-02-122-7/+139
generated by cgit (git 2.34.1) at 2024-05-19 20:46:31 +0000