From 7cd945fb3db868bc28d4c0dce101b03b2de9ffe3 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 29 Sep 2006 15:47:49 +0000
Subject: args implicites dans Field

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

(limited to 'contrib/setoid_ring/RealField.v')

diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index 256354d78c..194c396ea8 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -1,5 +1,5 @@
 Require Import Raxioms.
-Require Export Rdefinitions.
+Require Import Rdefinitions.
 Require Import Ring Field.
 
 Open Local Scope R_scope.
@@ -22,8 +22,7 @@ constructor.
  exact Rplus_opp_r.
 Qed.
 
-Lemma Rfield :
-  field_theory R 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
+Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
 Proof.
 constructor.
  exact RTheory.
@@ -101,6 +100,6 @@ Lemma Zeq_bool_complete : forall x y,
   InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
   InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
   Zeq_bool x y = true.
-Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0.
+Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
 
 Add Field RField : Rfield (infinite Zeq_bool_complete).
-- 
cgit v1.2.3