aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Sum.v
Commit message (Expand)AuthorAge
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* 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
* 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