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/field/countalg.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/field/countalg.v')

diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v
index 46ce3a3..95d28cb 100644
--- a/mathcomp/field/countalg.v
+++ b/mathcomp/field/countalg.v
@@ -957,7 +957,7 @@ pose incEp E i j :=
   let v := map_poly (EtoInc E i) (tagged E j) in
   if decode j is [:: i1; k] then
     if i1 == i then odflt v (unpickle k) else v
-  else v. 
+  else v.
 pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0.
 pose E i := tag (E_ i); pose Krep := {i : nat & E i}.
 pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} :=
-- 
cgit v1.2.3