aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra/SubsetoidRing.v
Commit message (Collapse)AuthorAge
* subsetoid_ring: don't ask for false thingsGravatar Jason Gross2018-03-12
| | | | | We can't actually prove the previous okness lemmas in SimplyTypedArithmetic, so we instead ask for exactly what we need.
* Add Algebra.SubsetoidRingGravatar Jason Gross2018-03-12