From c0a3544d6351e19c695951796bcee838671d1098 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:15 +0000 Subject: Modularization of BinPos + fixes in Stdlib BinPos now contain a sub-module Pos, in which are placed functions like add (ex-Pplus), mul (ex-Pmult), ... and properties like add_comm, add_assoc, ... In addition to the name changes, the organisation is changed quite a lot, to try to take advantage more of the orders < and <= instead of speaking only of the comparison function. The main source of incompatibilities in scripts concerns this compare: Pos.compare is now a binary operation, expressed in terms of the ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg), this ternary version being called now Pos.compare_cont. As for everything else, compatibility notations (only parsing) are provided. But notations "_ ?= _" on positive will have to be edited, since they now point to Pos.compare. We also make the sub-module Pos to be directly an OrderedType, and include results about min and max. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/QArith/Qpower.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/QArith') diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 765bc45fa..188a74fdd 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -136,7 +136,7 @@ Proof. intros a [|n|n] [|m|m] H; simpl; try ring; try rewrite Qpower_plus_positive; try apply Qinv_mult_distr; try reflexivity; -case_eq ((n ?= m)%positive Eq); intros H0; simpl; +case_eq ((n ?= m)%positive); intros H0; simpl; try rewrite Qpower_minus_positive; try rewrite (Pcompare_Eq_eq _ _ H0); try (field; try split; apply Qpower_not_0_positive); -- cgit v1.2.3