aboutsummaryrefslogtreecommitdiffstats
path: root/src/SMT_terms.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-171-1/+1
|\
| * Update copyrightChantal Keller2022-02-161-1/+1
* | Use the Register mechanism (#104)ckeller2022-02-151-0/+73
* | Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2021-10-211-60/+44
|\|
| * Better use of the typeclass mechanismChantal Keller2021-10-211-60/+44
* | use native integers (#96)vblot2021-07-071-92/+102
* | Merge remote-tracking branch 'remotes/origin/master' into coq-8.10Chantal Keller2021-06-021-9/+9
|\|
| * Type back in CompDec (for efficiency reasons)Chantal Keller2021-06-021-9/+9
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-261-1/+1
|\|
| * Update copyrightChantal Keller2021-05-261-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-251-69/+63
|\|
| * CompDec clean-up (#93)ckeller2021-05-251-69/+63
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-07-201-45/+4
|\|
| * Define substitution conformly to SMT-LIBChantal Keller2020-07-201-45/+4
* | Hints in databasesChantal Keller2020-01-281-9/+9
|/
* 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