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/algebra | |
| 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/algebra')
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 486b12e..8e384a8 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1546,7 +1546,7 @@ End Exports. End Lmodule. Import Lmodule.Exports. -Definition scale (R : ringType) (V : lmodType R) := +Definition scale (R : ringType) (V : lmodType R) : R -> V -> V := Lmodule.scale (Lmodule.class V). Local Notation "*:%R" := (@scale _ _). |