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

(limited to 'mathcomp/real_closed/realalg.v')

diff --git a/mathcomp/real_closed/realalg.v b/mathcomp/real_closed/realalg.v
index 69fb9c4..0cbba9f 100644
--- a/mathcomp/real_closed/realalg.v
+++ b/mathcomp/real_closed/realalg.v
@@ -229,7 +229,7 @@ Lemma root_inv_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) :
 Proof.
 rewrite /div_algcreal; case: eq_algcreal_dec=> [/(_ x_neq0)|x_neq0'] //=.
 case: simplify_algcreal=> x' px'0_neq0 [x'_neq0 eq_xx'].
-apply: is_root_annul_creal;rewrite /= -(@eq_creal_inv _ _ _ x_neq0) //.
+apply: is_root_annul_creal; rewrite /= -(@eq_creal_inv _ _ _ x_neq0) //.
 by apply: eq_crealP; exists m0=> * /=; rewrite div1r subrr normr0.
 Qed.
 
-- 
cgit v1.2.3