aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Tests_lfsc_tactics.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2022-02-171-1/+1
|\
| * Update copyrightChantal Keller2022-02-161-1/+1
* | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-07-071-7/+7
|/
* Update copyrightChantal Keller2021-05-261-1/+1
* Take hypotheses from the local context (#91)ckeller2021-04-261-5/+5
* Convert hypotheses from Prop to bool (#89)ckeller2021-04-211-2/+2
* Example of groups in unit testsChantal Keller2021-02-231-18/+37
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-1/+89
* Testing BV subtractionChantal Keller2020-07-201-0/+16
* Test asynchronous and make the selected lemmas persistant (#66)ckeller2020-03-261-72/+83
* 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-121-0/+705