aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native/smtcoq_plugin_native.ml4
Commit message (Expand)AuthorAgeFilesLines
* getting rid of native-coq (#95)vblot2021-05-281-99/+0
* Update copyrightChantal Keller2021-05-261-1/+1
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-121-4/+6
* Merge from LFSC (#26)ckeller2019-01-281-8/+34
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-1/+9
* Command to bypass typechecking when generating a zchaff theoremChantal Keller2017-11-141-0/+7
* Corrected a bug with holes in proofs (for native-coq)Chantal Keller2016-10-071-2/+2
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-281-2/+2
* Now, Coq 8.5 is the defaultChantal Keller2016-05-011-0/+56