diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-29 15:47:49 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-29 15:47:49 +0000 |
| commit | 7cd945fb3db868bc28d4c0dce101b03b2de9ffe3 (patch) | |
| tree | f2c63d443f005119985d50c22efa335e55ed5c92 /theories/QArith | |
| parent | f8d64ae9e9b9a3c3a3010d1a9e97e979ee63b162 (diff) | |
args implicites dans Field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9192 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/Qcanon.v | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 65644d0ea..bbe51c45c 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. |