diff options
Diffstat (limited to 'theories/QArith/Qfield.v')
| -rw-r--r-- | theories/QArith/Qfield.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 9841ef89..fbfae55c 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qfield.v 11208 2008-07-04 16:57:46Z letouzey $ i*) +(*i $Id$ i*) Require Export Field. Require Export QArith_base. @@ -73,15 +73,15 @@ Ltac Qpow_tac t := | _ => NotConstant end. -Add Field Qfield : Qsft - (decidable Qeq_bool_eq, +Add Field Qfield : Qsft + (decidable Qeq_bool_eq, completeness Qeq_eq_bool, - constants [Qcst], + constants [Qcst], power_tac Qpower_theory [Qpow_tac]). (** Exemple of use: *) -Section Examples. +Section Examples. Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). intros. @@ -89,7 +89,7 @@ Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). Qed. Let ex2 : forall x y : Q, x+y == y+x. - intros. + intros. ring. Qed. |