From 8ea798d3166b78b1969b2edcd4986bdaa3caa236 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 2 Feb 2005 21:33:14 +0000
Subject: The statement of the compatibility theorem for addition and
 multiplication have been changed to match the new statement used by Add
 Setoid.

NOTE: this reveals a missing check in the code. Indeed, "Add Setoid Ring"
does not check if the provided compatibility theorems have the expected type.
To be done in a future commit.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6662 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Setoid_ring_normalize.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'contrib/ring/Setoid_ring_normalize.v')

diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index aa6d95eabf..96ba632fc8 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -37,14 +37,14 @@ Variable S : Setoid_Theory A Aequiv.
 
 Add Setoid A Aequiv S as Asetoid.
 
-Variable
-  plus_morph :
-    forall a a0 a1 a2:A,
-      Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Aplus a a1) (Aplus a0 a2).
-Variable
-  mult_morph :
-    forall a a0 a1 a2:A,
-      Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Amult a a1) (Amult a0 a2).
+Variable plus_morph :
+ forall a a0:A, Aequiv a a0 ->
+   forall a1 a2:A, Aequiv a1 a2 ->
+     Aequiv (Aplus a a1)  (Aplus a0 a2).
+Variable mult_morph :
+ forall a a0:A, Aequiv a a0 ->
+   forall a1 a2:A, Aequiv a1 a2 ->
+     Aequiv (Amult a a1) (Amult a0 a2).
 Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0).
 
 Add Morphism Aplus : Aplus_ext.
-- 
cgit v1.2.3