From fafd4dac5315e1d4e071b0044a50a16360b31964 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 23 Nov 2017 16:33:36 +0100
Subject: running semi-automated linting on the whole library

---
 mathcomp/attic/galgebra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/attic/galgebra.v')

diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v
index 4902a47..16bbe1e 100644
--- a/mathcomp/attic/galgebra.v
+++ b/mathcomp/attic/galgebra.v
@@ -55,11 +55,11 @@ Definition mulrg v1 v2 :=
  GAlg ([ffun g => \sum_(k : gT) (v1 k) * (v2 ((k^-1) * g)%g)]).
 
 Lemma addrgA : associative addrg.
-Proof. 
+Proof.
 by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrA.
 Qed.
 Lemma addrgC : commutative addrg.
-Proof. 
+Proof.
 by move=> *; apply: val_inj; apply/ffunP=> ?; rewrite !ffunE addrC.
 Qed.
 Lemma addr0g : left_id g0 addrg.
-- 
cgit v1.2.3