aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
Commit message (Collapse)AuthorAge
* Add some move/transport eq lemmasJason Gross2019-04-22
|
* Add push_rew_fun_depJason Gross2019-04-22
|
* Add PrimitiveSigmaJason Gross2018-09-14
|
* Minor refactoringJason Gross2018-06-13
| | | | Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction
* Don't rely on autogenerated namesJason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Add ap_transport to Equality.vJason Gross2017-04-02
|
* Add match commutation lemmasJason Gross2017-01-23
|
* Minor additionsJason Gross2017-01-23
|
* Util.Equality on 8.4Andres Erbsen2016-08-04
|
* Add documentation: Equality, HProp, Isomorphism, Sigma (#41)Jason Gross2016-08-01
| | | | | | * Add doc: Equality, HProp, Isomorphism, Sigma * Update documentation with suggestions from Andres
* Fixes for Coq 8.4Jason Gross2016-08-01
|
* Add a lemma about hprop and eqJason Gross2016-07-29
|
* Set Asymmetric Patterns, add util lemmas about sigJason Gross2016-07-29