aboutsummaryrefslogtreecommitdiffstats
path: root/src/SMT_terms.v
Commit message (Expand)AuthorAgeFilesLines
* Better use of the typeclass mechanismChantal Keller2021-10-211-60/+44
* Type back in CompDec (for efficiency reasons)Chantal Keller2021-06-021-9/+9
* Update copyrightChantal Keller2021-05-261-1/+1
* CompDec clean-up (#93)ckeller2021-05-251-69/+63
* Define substitution conformly to SMT-LIBChantal Keller2020-07-201-45/+4
* V8.9 (#43)ckeller2019-03-151-2/+2
* V8.8 (#42)ckeller2019-03-111-2/+2
* V8.7 (#36)ckeller2019-02-141-5/+12
* Merge from LFSC (#26)ckeller2019-01-281-163/+1503
* formattingQuentin Garchery2018-10-271-1/+0
* Zeq_bool -> Z.eqbQuentin Garchery2018-10-271-7/+7
* Updating of the copyrightChantal Keller2016-04-271-2/+2
* The tactic "verit" generates more user-friendly subgoalsChantal Keller2016-04-261-9/+3
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-0/+16
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-0/+5
* More on the support for standard Coq (not working yet)Chantal Keller2015-02-101-3/+2
* Initial import of SMTCoq v1.2Chantal Keller2015-01-121-0/+1308