From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 plugins/setoid_ring/Ring_theory.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/setoid_ring/Ring_theory.v')

diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index af43b0ab..4f05f0d4 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -28,6 +28,8 @@ Reserved Notation "x == y" (at level 70, no associativity).
 End RingSyntax.
 Import RingSyntax.
 
+(* Set Universe Polymorphism. *)
+
 Section Power.
  Variable R:Type.
  Variable rI : R.
@@ -252,6 +254,7 @@ Section ALMOST_RING.
 
  Section SEMI_RING.
  Variable SReqe : sring_eq_ext radd rmul req.
+
    Add Morphism radd : radd_ext1.  exact (SRadd_ext SReqe). Qed.
    Add Morphism rmul : rmul_ext1.  exact (SRmul_ext SReqe). Qed.
  Variable SRth : semi_ring_theory 0 1 radd rmul req.
@@ -503,7 +506,6 @@ Qed.
 
 End ALMOST_RING.
 
-
 Section AddRing.
 
 (* Variable R : Type.
@@ -528,7 +530,6 @@ Inductive ring_kind : Type :=
     (_ : ring_morph rO rI radd rmul rsub ropp req
                     cO cI cadd cmul csub copp ceqb phi).
 
-
 End AddRing.
 
 
-- 
cgit v1.2.3