aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests
Commit message (Collapse)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
| | | | | | | | some cases)
* | 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, ↵Chantal Keller2021-04-261-4/+13
| | | | | | | | when possible
* | 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
| | | | | | | | | | * The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context * `prop2bool_hyps` also apply to hypotheses not in the local context * Second strategy for vauto (still incomplete)
* | 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
| | | | | | | | | | | | | | * This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed. * Some current limitations are detailed in src/PropToBool.v. * Partially enhances #30 .
* | 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
| | | | | Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
* Reify polymorphic termsckeller2021-01-051-0/+10
| | | A polymorphic term is now reified as a whole of the term applied to one or many types. The same polymorphic term applied to different types is reified as different monomorphic terms.
* 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
| | | | | | | * Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though) * Make the selected lemmas persistant Co-authored-by: Chantal Keller <Chantal.Keller@lri.fr>
* 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
| | | * Better error message for failing tactics with native-coq
* V8.7 (#36)ckeller2019-02-142-40/+16
| | | Port SMTCoq to Coq-8.7
* Cleaning (#35)QGarchery2019-02-122-7/+139
| | | | | Removing tests from the example folder More commentaries in Example.v
generated by cgit (git 2.34.1) at 2024-06-02 20:57:47 +0000