diff options
Diffstat (limited to 'theories')
| -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 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. |