aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Sum.v
Commit message (Collapse)AuthorAge
* Don't change sumbool eq hypothesis unless both sides are constructorsGravatar Jason Gross2017-01-30
|
* Fix typosGravatar Jason Gross2017-01-30
|
* Add Util.SumboolGravatar Jason Gross2017-01-30
|
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
| | | | This way they won't become ambiguous if we add new files
* Add decidable instances for sumwise and fieldwiseGravatar Jason Gross2016-06-27
|
* Add a tactic for dealing with equalities of [sum]Gravatar Jason Gross2016-06-27
|
* Add equality on sum typesGravatar Jason Gross2016-06-23