index
:
smtcoq
coq-8.13
Fork of https://github.com/smtcoq/smtcoq.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
unit-tests
/
Tests_verit_tactics.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Update copyright
Chantal Keller
2021-05-26
1
-1
/
+1
*
Another silent change of veriT...
Chantal Keller
2021-05-06
1
-0
/
+22
*
Example for #92
Chantal Keller
2021-05-06
1
-0
/
+12
*
CompDec on interpreted type
Chantal Keller
2021-05-05
1
-0
/
+35
*
Reify applied polymorphic terms with compdec
Chantal Keller
2021-05-05
1
-0
/
+31
*
Solve a bug when reifying under a binder
Chantal Keller
2021-04-28
1
-0
/
+14
*
Equality between Booleans should be changed for hypotheses
Chantal Keller
2021-04-26
1
-0
/
+11
*
CompDec are automatically discharged when generated by the OCaml tactic, when...
Chantal Keller
2021-04-26
1
-4
/
+13
*
Take hypotheses from the local context (#91)
ckeller
2021-04-26
1
-52
/
+46
*
Convert hypotheses from Prop to bool (#89)
ckeller
2021-04-21
1
-38
/
+171
*
The examples on lists uses the true list type
Chantal Keller
2021-02-23
1
-10
/
+5
*
Link equality on uninterpreted sorts with SMT equality (#86)
ckeller
2021-02-23
1
-26
/
+129
*
Reify polymorphic terms
ckeller
2021-01-05
1
-0
/
+10
*
Close #10
Chantal Keller
2020-05-15
1
-0
/
+18
*
Test asynchronous and make the selected lemmas persistant (#66)
ckeller
2020-03-26
1
-106
/
+118
*
Separate unit tests into vernac and tactics
Chantal Keller
2019-04-12
1
-0
/
+966