aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Tests_verit_tactics.v
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
* Clean-upChantal Keller2022-04-141-0/+64
* Update copyrightChantal Keller2022-02-161-1/+1
* Solved bug in delayed ComDecChantal Keller2021-12-071-0/+23
* More bad instanciations by veritChantal Keller2021-11-151-0/+26
* Two examples showing that prenex dependency is handled, but not non-prenex oneChantal Keller2021-10-141-0/+43
* vauto is now complete w.r.t. symmetry of equality (but may be exponential in ...Chantal Keller2021-09-201-0/+37
* Solve bug in prop2boolChantal Keller2021-09-171-0/+6
* Update copyrightChantal Keller2021-05-261-1/+1
* Another silent change of veriT...Chantal Keller2021-05-061-0/+22
* Example for #92Chantal Keller2021-05-061-0/+12
* CompDec on interpreted typeChantal Keller2021-05-051-0/+35
* Reify applied polymorphic terms with compdecChantal Keller2021-05-051-0/+31
* Solve a bug when reifying under a binderChantal Keller2021-04-281-0/+14
* Equality between Booleans should be changed for hypothesesChantal Keller2021-04-261-0/+11
* CompDec are automatically discharged when generated by the OCaml tactic, when...Chantal Keller2021-04-261-4/+13
* Take hypotheses from the local context (#91)ckeller2021-04-261-52/+46
* Convert hypotheses from Prop to bool (#89)ckeller2021-04-211-38/+171
* 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-231-26/+129
* Reify polymorphic termsckeller2021-01-051-0/+10
* Close #10Chantal Keller2020-05-151-0/+18
* Test asynchronous and make the selected lemmas persistant (#66)ckeller2020-03-261-106/+118
* Separate unit tests into vernac and tacticsChantal Keller2019-04-121-0/+966
generated by cgit (git 2.34.1) at 2024-05-18 19:15:19 +0000