Imported Upstream version 8.5~beta1+dfsg

12 files changed, 37 insertions, 36 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 79e81771..f85222df 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -80,13 +80,13 @@ Module KeyDecidableType(D:DecidableType).
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
-    unfold eqke; induction 1; intuition.
+    unfold eqke; induction 1; intuition. 
   Qed.
   Hint Resolve InA_eqke_eqk.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
-   intros; apply InA_eqA with p; auto with *.
+   intros; apply InA_eqA with p; auto with *. 
   Qed.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
index 971fcd7f..163a40f2 100644
--- a/theories/Structures/DecidableTypeEx.v
+++ b/theories/Structures/DecidableTypeEx.v
@@ -88,7 +88,7 @@ Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
  unfold eq, D1.eq, D2.eq in *; simpl;
  (left; f_equal; auto; fail) ||
- (right; intro H; injection H; auto).
+ (right; injection; auto).
  Defined.
 
 End PairUsualDecidableType.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index eb537385..747d03f8 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -126,14 +126,14 @@ Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
       [EqualityType] and [DecidableType] *)
 
 Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
- Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
- Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
- Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+ Definition eq_refl := F.eq_equiv.(@Equivalence_Reflexive _ _). 
+ Definition eq_sym := F.eq_equiv.(@Equivalence_Symmetric _ _).
+ Definition eq_trans := F.eq_equiv.(@Equivalence_Transitive _ _).
 End BackportEq.
 
 Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
  Instance eq_equiv : Equivalence E.eq.
- Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+ Proof. exact (Build_Equivalence _ F.eq_refl F.eq_sym F.eq_trans). Qed.
 End UpdateEq.
 
 Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index c69885b4..11d94c11 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -166,7 +166,7 @@ Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
  unfold eq, D1.eq, D2.eq in *; simpl;
  (left; f_equal; auto; fail) ||
- (right; intro H; injection H; auto).
+ (right; intros [=]; auto).
  Defined.
 
 End PairUsualDecidableType.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index ffd0649a..ac52d1bb 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -110,7 +110,7 @@ Proof.
  intros x x' Hx y y' Hy.
  assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
  set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
- rewrite <- Hx, <- Hy in *.
+ rewrite <- Hx, <- Hy in *. 
  destruct (lt_total x y); intuition order.
 Qed.
 
@@ -440,7 +440,7 @@ Qed.
 
 Lemma max_min_antimono f :
  Proper (eq==>eq) f ->
- Proper (le==>inverse le) f ->
+ Proper (le==>flip le) f ->
  forall x y, max (f x) (f y) == f (min x y).
 Proof.
  intros Eqf Lef x y.
@@ -452,7 +452,7 @@ Qed.
 
 Lemma min_max_antimono f :
  Proper (eq==>eq) f ->
- Proper (le==>inverse le) f ->
+ Proper (le==>flip le) f ->
  forall x y, min (f x) (f y) == f (max x y).
 Proof.
  intros Eqf Lef x y.
@@ -557,11 +557,11 @@ Module UsualMinMaxLogicalProperties
   forall x y, min (f x) (f y) = f (min x y).
  Proof. intros; apply min_mono; auto. congruence. Qed.
 
- Lemma min_max_antimonotone f : Proper (le ==> inverse le) f ->
+ Lemma min_max_antimonotone f : Proper (le ==> flip le) f ->
   forall x y, min (f x) (f y) = f (max x y).
  Proof. intros; apply min_max_antimono; auto. congruence. Qed.
 
- Lemma max_min_antimonotone f : Proper (le ==> inverse le) f ->
+ Lemma max_min_antimonotone f : Proper (le ==> flip le) f ->
   forall x y, max (f x) (f y) = f (min x y).
  Proof. intros; apply max_min_antimono; auto. congruence. Qed.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 75578195..cc8c2261 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -49,7 +49,7 @@ Module Type OrderedType.
   Include MiniOrderedType.
 
   (** A [eq_dec] can be deduced from [compare] below. But adding this
-     redundant field allows to see an OrderedType as a DecidableType. *)
+     redundant field allows seeing an OrderedType as a DecidableType. *)
   Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 
 End OrderedType.
@@ -85,16 +85,16 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
   Proof.
-   intros; destruct (compare x z); auto.
+   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
    elim (lt_not_eq H); apply eq_trans with z; auto.
-   elim (lt_not_eq (lt_trans l H)); auto.
+   elim (lt_not_eq (lt_trans Hlt H)); auto.
   Qed.
 
   Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
   Proof.
-   intros; destruct (compare x z); auto.
+   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.
    elim (lt_not_eq H0); apply eq_trans with x; auto.
-   elim (lt_not_eq (lt_trans H0 l)); auto.
+   elim (lt_not_eq (lt_trans H0 Hlt)); auto.
   Qed.
 
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
@@ -225,7 +225,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
 Proof. exact (InfA_ltA lt_strorder). Qed.
 
 Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
 
 Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
 Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
@@ -398,7 +398,7 @@ Module KeyOrderedType(O:OrderedType).
   Qed.
 
   Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed.
+  Proof. exact (InfA_eqA eqk_equiv ltk_compat). Qed.
 
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 83130deb..3c6afc7b 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -279,7 +279,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   Proof.
   induction x; destruct y.
   - (* I I *)
-    destruct (IHx y).
+    destruct (IHx y) as [l|e|g].
     apply LT; auto.
     apply EQ; rewrite e; red; auto.
     apply GT; auto.
@@ -290,7 +290,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   - (* O I *)
     apply LT; simpl; auto.
   - (* O O *)
-    destruct (IHx y).
+    destruct (IHx y) as [l|e|g].
     apply LT; auto.
     apply EQ; rewrite e; red; auto.
     apply GT; auto.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 1d025439..724690b4 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -15,11 +15,11 @@ Unset Strict Implicit.
 (** First, signatures with only the order relations *)
 
 Module Type HasLt (Import T:Typ).
-  Parameter Inline lt : t -> t -> Prop.
+  Parameter Inline(40) lt : t -> t -> Prop.
 End HasLt.
 
 Module Type HasLe (Import T:Typ).
-  Parameter Inline le : t -> t -> Prop.
+  Parameter Inline(40) le : t -> t -> Prop.
 End HasLe.
 
 Module Type EqLt := Typ <+ HasEq <+ HasLt.
@@ -95,7 +95,7 @@ Module Type OrderedTypeFull' :=
  OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation.
 
 (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
-  But adding this redundant field allows to see an [OrderedType] as a
+  But adding this redundant field allows seeing an [OrderedType] as a
   [DecidableType]. *)
 
 (** * Versions with [eq] being the usual Leibniz equality of Coq *)
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index e071d053..acc7c767 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -11,16 +11,16 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-Require Import Orders NPeano POrderedType NArith
- ZArith RelationPairs EqualitiesFacts.
+Require Import Orders PeanoNat POrderedType BinNat BinInt
+ RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
 
 (** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *)
 
-Module Nat_as_OT := NPeano.Nat.
-Module Positive_as_OT := POrderedType.Positive_as_OT.
+Module Nat_as_OT := PeanoNat.Nat.
+Module Positive_as_OT := BinPos.Pos.
 Module N_as_OT := BinNat.N.
 Module Z_as_OT := BinInt.Z.
 
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 2e9c0cf5..88fbd8c1 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -31,7 +31,7 @@ Module Type CompareFacts (Import O:DecStrOrder').
 
  Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y.
  Proof.
- case compare_spec; intro H; split; try easy; intro LT;
+  case compare_spec; intro H; split; try easy; intro LT;
   contradict LT; rewrite H; apply irreflexivity.
  Qed.
 
@@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull').
  Instance le_order : PartialOrder eq le.
  Proof. compute; iorder. Qed.
 
- Instance le_antisym : Antisymmetric _ eq le.
+ Instance le_antisym : Antisymmetric eq le.
  Proof. apply partial_order_antisym; auto with *. Qed.
 
  Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index f83b6377..059992f5 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -32,7 +32,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
 Proof. exact (InfA_ltA lt_strorder). Qed.
 
 Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
 
 Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
 Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 68ffc379..475a25a4 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -29,7 +29,7 @@ Set Implicit Arguments.
     [le x y -> le y z -> le x z].
 *)
 
-Inductive ord := OEQ | OLT | OLE.
+Inductive ord : Set := OEQ | OLT | OLE.
 Definition trans_ord o o' :=
  match o, o' with
  | OEQ, _ => o'
@@ -70,7 +70,7 @@ Lemma le_refl : forall x, x<=x.
 Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed.
 
 Lemma lt_irrefl : forall x, ~ x<x.
-Proof. intros; apply StrictOrder_Irreflexive. Qed.
+Proof. intros. apply StrictOrder_Irreflexive. Qed.
 
 (** Symmetry rules *)
 
@@ -100,8 +100,9 @@ Local Notation "#" := interp_ord.
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
 Proof.
-destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition;
- subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+destruct o, o'; simpl; intros x y z;
+rewrite ?P.le_lteq; intuition auto;
+subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.
 
 Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.