Merge pull request #223 from math-comp/fix/compat-notation

[warnings] -w "+compatibility-notation" clean

3 files changed, 9 insertions, 9 deletions

diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index fcd6c2d..5d78cac 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -354,10 +354,10 @@ Lemma extend_algC_subfield_aut (Qs : fieldExtType rat)
 Proof.
 pose numF_inj (Qr : fieldExtType rat) := {rmorphism Qr -> algC}.
 pose subAut := {Qr : _ & numF_inj Qr * {lrmorphism Qr -> Qr}}%type.
-pose SubAut := existS _ _ (_, _) : subAut.
-pose Sdom (mu : subAut) := projS1 mu.
-pose Sinj (mu : subAut) : {rmorphism Sdom mu -> algC} := (projS2 mu).1.
-pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projS2 mu).2.
+pose SubAut := existT _ _ (_, _) : subAut.
+pose Sdom (mu : subAut) := projT1 mu.
+pose Sinj (mu : subAut) : {rmorphism Sdom mu -> algC} := (projT2 mu).1.
+pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projT2 mu).2.
 have SinjZ Qr (QrC : numF_inj Qr) a x: QrC (a *: x) = QtoC a * QrC x.
   rewrite mulrAC; apply: canRL (mulfK _) _.
     by rewrite intr_eq0 denq_neq0.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 01ce7a9..7721f0e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -784,9 +784,9 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
 
 End OptionEqType.
 
-Definition tag := projS1.
-Definition tagged I T_ :  forall u, T_(tag u) := @projS2 I [eta T_].
-Definition Tagged I i T_ x := @existS I [eta T_] i x.
+Definition tag := projT1.
+Definition tagged I T_ :  forall u, T_(tag u) := @projT2 I [eta T_].
+Definition Tagged I i T_ x := @existT I [eta T_] i x.
 Arguments Tagged [I i].
 Prenex Implicits tag tagged Tagged.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index b7ff16c..f7cd700 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1445,7 +1445,7 @@ End NatTrec.
 
 Notation natTrecE := NatTrec.trecE.
 
-Lemma eq_binP : Equality.axiom Ndec.Neqb.
+Lemma eq_binP : Equality.axiom N.eqb.
 Proof.
 move=> p q; apply: (iffP idP) => [|<-]; last by case: p => //; elim.
 by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //=; case/IHp=> ->.
@@ -1499,7 +1499,7 @@ case=> //=; elim=> //= p; case: (nat_of_pos p) => //= n [<-].
 by rewrite natTrecE addnS /= addnS {2}addnn; elim: {1 3}n.
 Qed.
 
-Lemma nat_of_succ_gt0 p : Psucc p = p.+1 :> nat.
+Lemma nat_of_succ_gt0 p : Pos.succ p = p.+1 :> nat.
 Proof. by elim: p => //= p ->; rewrite !natTrecE. Qed.
 
 Lemma nat_of_addn_gt0 p q : (p + q)%positive = p + q :> nat.