| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
| |
So that it doesn't interfere with [~> R] and [A ~> B].
|
| |
|
|
|
|
|
|
| |
We don't need both of them. We keep the definition of pointwise2
because it's needed for reification to work, and we keep the name of
fieldwise because it's used in more places. This closes #137.
|
| |
|
| |
|
|
As per @andres-erbsen's comments at
https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565223,
https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565200
|