diff options
| author | Kazuhiko Sakaguchi | 2019-10-26 16:32:30 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-10-26 16:32:30 +0200 |
| commit | a4d04cdad0a52db675eeab21dec3d46468ea657c (patch) | |
| tree | 7847e0038456471e3a553da2cc90da587d641038 /mathcomp/ssreflect/path.v | |
| parent | 9ec6b02e673d0808b3ba4a6c4f849405bf222ae1 (diff) | |
Add an explicit type annotation to GRing.scale
`V` was wrongly eta-expanded before:
GRing.scale
: forall (R : ringType) (V : lmodType R),
R -> GRing.Zmodule.Pack (GRing.Lmodule.class V) ->
GRing.Zmodule.Pack (GRing.Lmodule.class V)
Diffstat (limited to 'mathcomp/ssreflect/path.v')
0 files changed, 0 insertions, 0 deletions