diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 56 |
1 files changed, 29 insertions, 27 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index cf7397b5..12413453 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. + Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. Infix "-" := Z.sub : Z_scope. @@ -1569,40 +1571,40 @@ End Z2Pos. Notation Zdouble_plus_one := Z.succ_double (only parsing). Notation Zdouble_minus_one := Z.pred_double (only parsing). -Notation Zdouble := Z.double (compat "8.6"). +Notation Zdouble := Z.double (compat "8.7"). Notation ZPminus := Z.pos_sub (only parsing). -Notation Zsucc' := Z.succ (compat "8.6"). -Notation Zpred' := Z.pred (compat "8.6"). -Notation Zplus' := Z.add (compat "8.6"). +Notation Zsucc' := Z.succ (compat "8.7"). +Notation Zpred' := Z.pred (compat "8.7"). +Notation Zplus' := Z.add (compat "8.7"). Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) -Notation Zopp := Z.opp (compat "8.6"). -Notation Zsucc := Z.succ (compat "8.6"). -Notation Zpred := Z.pred (compat "8.6"). +Notation Zopp := Z.opp (compat "8.7"). +Notation Zsucc := Z.succ (compat "8.7"). +Notation Zpred := Z.pred (compat "8.7"). Notation Zminus := Z.sub (only parsing). Notation Zmult := Z.mul (only parsing). -Notation Zcompare := Z.compare (compat "8.6"). -Notation Zsgn := Z.sgn (compat "8.6"). -Notation Zle := Z.le (compat "8.6"). -Notation Zge := Z.ge (compat "8.6"). -Notation Zlt := Z.lt (compat "8.6"). -Notation Zgt := Z.gt (compat "8.6"). -Notation Zmax := Z.max (compat "8.6"). -Notation Zmin := Z.min (compat "8.6"). -Notation Zabs := Z.abs (compat "8.6"). -Notation Zabs_nat := Z.abs_nat (compat "8.6"). -Notation Zabs_N := Z.abs_N (compat "8.6"). +Notation Zcompare := Z.compare (compat "8.7"). +Notation Zsgn := Z.sgn (compat "8.7"). +Notation Zle := Z.le (compat "8.7"). +Notation Zge := Z.ge (compat "8.7"). +Notation Zlt := Z.lt (compat "8.7"). +Notation Zgt := Z.gt (compat "8.7"). +Notation Zmax := Z.max (compat "8.7"). +Notation Zmin := Z.min (compat "8.7"). +Notation Zabs := Z.abs (compat "8.7"). +Notation Zabs_nat := Z.abs_nat (compat "8.7"). +Notation Zabs_N := Z.abs_N (compat "8.7"). Notation Z_of_nat := Z.of_nat (only parsing). Notation Z_of_N := Z.of_N (only parsing). Notation Zind := Z.peano_ind (only parsing). -Notation Zopp_0 := Z.opp_0 (compat "8.6"). -Notation Zopp_involutive := Z.opp_involutive (compat "8.6"). -Notation Zopp_inj := Z.opp_inj (compat "8.6"). +Notation Zopp_0 := Z.opp_0 (compat "8.7"). +Notation Zopp_involutive := Z.opp_involutive (compat "8.7"). +Notation Zopp_inj := Z.opp_inj (compat "8.7"). Notation Zplus_0_l := Z.add_0_l (only parsing). Notation Zplus_0_r := Z.add_0_r (only parsing). Notation Zplus_comm := Z.add_comm (only parsing). Notation Zopp_plus_distr := Z.opp_add_distr (only parsing). -Notation Zopp_succ := Z.opp_succ (compat "8.6"). +Notation Zopp_succ := Z.opp_succ (compat "8.7"). Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing). Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing). Notation Zplus_assoc := Z.add_assoc (only parsing). @@ -1611,11 +1613,11 @@ Notation Zplus_reg_l := Z.add_reg_l (only parsing). Notation Zplus_succ_l := Z.add_succ_l (only parsing). Notation Zplus_succ_comm := Z.add_succ_comm (only parsing). Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing). -Notation Zsucc_inj := Z.succ_inj (compat "8.6"). -Notation Zsucc'_inj := Z.succ_inj (compat "8.6"). -Notation Zsucc'_pred' := Z.succ_pred (compat "8.6"). -Notation Zpred'_succ' := Z.pred_succ (compat "8.6"). -Notation Zpred'_inj := Z.pred_inj (compat "8.6"). +Notation Zsucc_inj := Z.succ_inj (compat "8.7"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.7"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.7"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.7"). +Notation Zpred'_inj := Z.pred_inj (compat "8.7"). Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing). Notation Zminus_0_r := Z.sub_0_r (only parsing). Notation Zminus_diag := Z.sub_diag (only parsing). |