1 files changed, 23 insertions, 23 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 5129a3ca..921e2d67 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,8 +23,6 @@ Require Export BinPosDef.
     are now defined in [BinNums.v] *)
 
 Local Open Scope positive_scope.
-Local Unset Boolean Equality Schemes.
-Local Unset Case Analysis Schemes.
 
 (** Every definitions and early properties about positive numbers
     are placed in a module [Pos] for qualification purpose. *)
@@ -578,21 +576,21 @@ Qed.
 
 Lemma iter_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B),
  (forall a, f (g a) = h (f a)) -> forall p a,
- f (iter p g a) = iter p h (f a).
+ f (iter g a p) = iter h (f a) p.
 Proof.
  induction p; simpl; intros; now rewrite ?H, ?IHp.
 Qed.
 
 Theorem iter_swap :
   forall p (A:Type) (f:A -> A) (x:A),
-    iter p f (f x) = f (iter p f x).
+    iter f (f x) p = f (iter f x p).
 Proof.
  intros. symmetry. now apply iter_swap_gen.
 Qed.
 
 Theorem iter_succ :
   forall p (A:Type) (f:A -> A) (x:A),
-    iter (succ p) f x = f (iter p f x).
+    iter f x (succ p) = f (iter f x p).
 Proof.
  induction p as [p IHp|p IHp|]; intros; simpl; trivial.
  now rewrite !IHp, iter_swap.
@@ -600,7 +598,7 @@ Qed.
 
 Theorem iter_add :
   forall p q (A:Type) (f:A -> A) (x:A),
-    iter (p+q) f x = iter p f (iter q f x).
+    iter f x (p+q) = iter f (iter f x q) p.
 Proof.
  induction p using peano_ind; intros.
  now rewrite add_1_l, iter_succ.
@@ -610,7 +608,7 @@ Qed.
 Theorem iter_invariant :
   forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
-    forall x:A, Inv x -> Inv (iter p f x).
+    forall x:A, Inv x -> Inv (iter f x p).
 Proof.
  induction p as [p IHp|p IHp|]; simpl; trivial.
  intros A f Inv H x H0. apply H, IHp, IHp; trivial.
@@ -651,7 +649,7 @@ Theorem sub_mask_carry_spec p q :
   sub_mask_carry p q = pred_mask (sub_mask p q).
 Proof.
   revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl;
-   try reflexivity; try rewrite IHp;
+   try reflexivity; rewrite ?IHp;
    destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto.
 Qed.
 
@@ -768,15 +766,15 @@ Definition switch_Eq c c' :=
  end.
 
 Lemma compare_cont_spec p q c :
-  compare_cont p q c = switch_Eq c (p ?= q).
+  compare_cont c p q = switch_Eq c (p ?= q).
 Proof.
   unfold compare.
   revert q c.
   induction p; destruct q; simpl; trivial.
   intros c.
-  rewrite 2 IHp. now destruct (compare_cont p q Eq).
+  rewrite 2 IHp. now destruct (compare_cont Eq p q).
   intros c.
-  rewrite 2 IHp. now destruct (compare_cont p q Eq).
+  rewrite 2 IHp. now destruct (compare_cont Eq p q).
 Qed.
 
 (** From this general result, we now describe particular cases
@@ -787,31 +785,31 @@ Qed.
 *)
 
 Theorem compare_cont_Eq p q c :
- compare_cont p q c = Eq -> c = Eq.
+ compare_cont c p q = Eq -> c = Eq.
 Proof.
   rewrite compare_cont_spec. now destruct (p ?= q).
 Qed.
 
 Lemma compare_cont_Lt_Gt p q :
-  compare_cont p q Lt = Gt <-> p > q.
+  compare_cont Lt p q = Gt <-> p > q.
 Proof.
   rewrite compare_cont_spec. unfold gt. destruct (p ?= q); now split.
 Qed.
 
 Lemma compare_cont_Lt_Lt p q :
-  compare_cont p q Lt = Lt <-> p <= q.
+  compare_cont Lt p q = Lt <-> p <= q.
 Proof.
   rewrite compare_cont_spec. unfold le. destruct (p ?= q); easy'.
 Qed.
 
 Lemma compare_cont_Gt_Lt p q :
-  compare_cont p q Gt = Lt <-> p < q.
+  compare_cont Gt p q = Lt <-> p < q.
 Proof.
   rewrite compare_cont_spec. unfold lt. destruct (p ?= q); now split.
 Qed.
 
 Lemma compare_cont_Gt_Gt p q :
-  compare_cont p q Gt = Gt <-> p >= q.
+  compare_cont Gt p q = Gt <-> p >= q.
 Proof.
   rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'.
 Qed.
@@ -876,13 +874,13 @@ Qed.
 (** Basic facts about [compare_cont] *)
 
 Theorem compare_cont_refl p c :
-  compare_cont p p c = c.
+  compare_cont c p p = c.
 Proof.
   now induction p.
 Qed.
 
 Lemma compare_cont_antisym p q c :
-  CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c).
+  CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p.
 Proof.
   revert q c.
   induction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl;
@@ -1840,6 +1838,8 @@ Qed.
 
 End Pos.
 
+Bind Scope positive_scope with Pos.t positive.
+
 (** Exportation of notations *)
 
 Infix "+" := Pos.add : positive_scope.
@@ -1903,7 +1903,7 @@ Notation Pdiv2 := Pos.div2 (compat "8.3").
 Notation Pdiv2_up := Pos.div2_up (compat "8.3").
 Notation Psize := Pos.size_nat (compat "8.3").
 Notation Psize_pos := Pos.size (compat "8.3").
-Notation Pcompare := Pos.compare_cont (compat "8.3").
+Notation Pcompare x y m := (Pos.compare_cont m x y) (compat "8.3").
 Notation Plt := Pos.lt (compat "8.3").
 Notation Pgt := Pos.gt (compat "8.3").
 Notation Ple := Pos.le (compat "8.3").
@@ -2062,11 +2062,11 @@ Lemma Pplus_one_succ_r p : Pos.succ p = p + 1.
 Proof (eq_sym (Pos.add_1_r p)).
 Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p.
 Proof (eq_sym (Pos.add_1_l p)).
-Lemma Pcompare_refl p : Pos.compare_cont p p Eq = Eq.
+Lemma Pcompare_refl p : Pos.compare_cont Eq p p = Eq.
 Proof (Pos.compare_cont_refl p Eq).
-Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont p q Eq = Eq -> p = q.
+Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont Eq p q = Eq -> p = q.
 Proof Pos.compare_eq.
-Lemma ZC4 p q : Pos.compare_cont p q Eq = CompOpp (Pos.compare_cont q p Eq).
+Lemma ZC4 p q : Pos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p).
 Proof (Pos.compare_antisym q p).
 Lemma Ppred_minus p : Pos.pred p = p - 1.
 Proof (eq_sym (Pos.sub_1_r p)).