From a4d04cdad0a52db675eeab21dec3d46468ea657c Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 26 Oct 2019 16:32:30 +0200
Subject: 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)
---
 mathcomp/algebra/ssralg.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 _ _).
-- 
cgit v1.2.3