aboutsummaryrefslogtreecommitdiffstats
path: root/src/QInst.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-061-0/+11
|\
| * Another silent change of veriT...Chantal Keller2021-05-061-0/+11
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-1/+42
|\|
| * Equality between Booleans should be changed for hypothesesChantal Keller2021-04-261-1/+42
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-12/+62
|\|
| * Take hypotheses from the local context (#91)ckeller2021-04-261-12/+62
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-02-231-10/+54
|\|
| * Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-10/+54
* | Compiles with Coq-8.10Chantal Keller2020-03-311-1/+1
* | Hint DB for QInstChantal Keller2020-01-281-1/+1
|/
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-121-0/+80