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
---
 theories/QArith/Qcanon.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'theories')

diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 65644d0eac..bbe51c45ce 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -526,7 +526,7 @@ constructor.
 Qed.
 
 Definition Qcft :
-  field_theory _ 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)).
+  field_theory 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)).
 Proof.
 constructor.
  exact Qcrt.
@@ -539,10 +539,6 @@ Add Field Qcfield : Qcft.
 
 (** A field tactic for rational numbers *)
 
-(*
-Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l
- with div:=Qcdiv.
-*)
 Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc.
 intros.
 field.
-- 
cgit v1.2.3