From a0f0f3982bf6991407f399ac430b354375a48dd2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Apr 2003 11:26:00 +0000
Subject: Alignement du comportement des implicites d'inductif en sortie de
 section sur celui des constantes

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

diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index c34c972f79..43b1f481e2 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -352,7 +352,7 @@ Unset Implicit Arguments.
 
 (* Section properties. *)
 
-Variable T : (Semi_Setoid_Ring_Theory A Aequiv Aplus Amult Aone Azero Aeq).
+Variable T : (Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq).
 
 Hint SSR_plus_sym_T := Resolve (SSR_plus_sym T).
 Hint SSR_plus_assoc_T := Resolve (SSR_plus_assoc T).
@@ -1009,7 +1009,7 @@ Section setoid_rings.
 Set Implicit Arguments.
 
 Variable vm : (varmap A).
-Variable T : (Setoid_Ring_Theory A Aequiv Aplus Amult Aone Azero Aopp Aeq).
+Variable T : (Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq).
 
 Hint STh_plus_sym_T := Resolve (STh_plus_sym T).
 Hint STh_plus_assoc_T := Resolve (STh_plus_assoc T).
-- 
cgit v1.2.3