Fix a missing section close in ZToRing

1 files changed, 6 insertions, 5 deletions

diff --git a/src/Algebra/ZToRing.v b/src/Algebra/ZToRing.v
index 8b9195d75..0c423222e 100644
--- a/src/Algebra/ZToRing.v
+++ b/src/Algebra/ZToRing.v
@@ -17,7 +17,7 @@ Section ZToRing.
   Definition ZToRing (x:Z) : R :=
     match x with
     | Z0 => Rzero
-    | Zpos p => natToRing (Pos.to_nat p) 
+    | Zpos p => natToRing (Pos.to_nat p)
     | Zneg p => Ropp (natToRing (Pos.to_nat p))
     end.
 
@@ -111,7 +111,7 @@ Section ZToRing.
       rewrite !ring_sub_definition.
       rewrite associative; reflexivity. }
   Qed.
-  
+
   Lemma ZToRing_inj_mul : forall a b,
       ZToRing (Z.mul a b) = Rmul (ZToRing a) (ZToRing b).
   Proof.
@@ -134,8 +134,8 @@ Section ZToRing.
       rewrite Ring.mul_opp_r,right_identity.
       reflexivity. }
   Qed.
-  
-  
+
+
   Lemma ZToRingHomom : @Ring.is_homomorphism
                          Z Z.eq Z.one Z.add Z.mul
                          R Req  Rone  Radd  Rmul
@@ -146,4 +146,5 @@ Section ZToRing.
     { repeat intro. cbv [Z.eq] in *. subst. reflexivity. }
     { apply ZToRing_inj_mul. }
     { simpl. rewrite left_identity; reflexivity. }
-  Qed.
\ No newline at end of file
+  Qed.
+End ZToRing.