aboutsummaryrefslogtreecommitdiffstats
path: root/src/SMT_terms.v
Commit message (Expand)AuthorAgeFilesLines
* Removed deprecated featuresChantal Keller2022-02-181-34/+34
* Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2022-02-171-1/+1
|\
| * Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2022-02-171-1/+1
| |\
| | * Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-171-1/+1
| | |\
| | | * Update copyrightChantal Keller2022-02-161-1/+1
* | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2022-02-151-0/+73
|\| | |
| * | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2022-02-151-0/+73
| |\| |
| | * | Use the Register mechanism (#104)ckeller2022-02-151-0/+73
* | | | Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13Chantal Keller2021-10-211-60/+44
|\| | |
| * | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2021-10-211-60/+44
| |\| |
| | * | 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
* | | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-07-071-92/+102
|\| | |
| * | | Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12Chantal Keller2021-07-071-92/+102
| |\| |
| | * | use native integers (#96)vblot2021-07-071-92/+102
* | | | Merge remote-tracking branch 'remotes/origin/coq-8.12' into coq-8.13Chantal Keller2021-06-071-9/+9
|\| | |
| * | | Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12Chantal Keller2021-06-071-9/+9
| |\| |
| | * | 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
* | | | Minor changes on the Coq partChantal Keller2021-05-261-1/+1
|/ / /
* | | Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12Chantal Keller2021-05-261-1/+1
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-261-1/+1
| |\|
| | * Update copyrightChantal Keller2021-05-261-1/+1
* | | Port the Coq partChantal 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