Require Export DoubleType.
Require Export PrimInt63.
Require Uint63.

Bind Scope int63_scope with int.

#[deprecated(since="8.14",note="Use Uint63.mod instead.")]
Notation mod := Uint63.mod (only parsing).
Notation lor := Uint63.lor (only parsing).
Notation land := Uint63.land (only parsing).
Notation lxor := Uint63.lxor (only parsing).

Import Uint63.

Notation size := size (only parsing).

Notation int := int (only parsing).
Notation lsl := lsl (only parsing).
Notation lsr := lsr (only parsing).
Notation add := add (only parsing).
Notation sub := sub (only parsing).
Notation mul := mul (only parsing).
Notation mulc := mulc (only parsing).
#[deprecated(since="8.14",note="Use Uint63.div instead.")]
Notation div := div (only parsing).
Notation eqb := eqb (only parsing).
#[deprecated(since="8.14",note="Use Uint63.ltb instead.")]
Notation ltb := ltb (only parsing).
#[deprecated(since="8.14",note="Use Uint63.leb instead.")]
Notation leb := leb (only parsing).

Module Import Int63NotationsInternalB.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "<<" := Uint63.lsl (at level 30, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix ">>" := Uint63.lsr (at level 30, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "land" := Uint63.land (at level 40, left associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "lor" := Uint63.lor (at level 40, left associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "lxor" := Uint63.lxor (at level 40, left associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "+" := Uint63.add : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "-" := Uint63.sub : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "*" := Uint63.mul : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "/" := Uint63.div : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "mod" := Uint63.mod (at level 40, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "=?" := Uint63.eqb (at level 70, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "<?" := Uint63.ltb (at level 70, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "<=?" := Uint63.leb (at level 70, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "≤?" := Uint63.leb (at level 70, no associativity) : int63_scope.
End Int63NotationsInternalB.

Notation digits := digits (only parsing).

#[deprecated(since="8.14",note="Use Uint63.max_int instead")]
Notation max_int := max_int (only parsing).

Notation get_digit := get_digit (only parsing).

Notation set_digit := set_digit (only parsing).

Notation is_zero := is_zero (only parsing).

Notation is_even := is_even (only parsing).

Notation bit := bit (only parsing).

Notation opp := opp (only parsing).

Notation oppcarry := oppcarry (only parsing).

Notation succ := succ (only parsing).

Notation pred := pred (only parsing).

Notation addcarry := addcarry (only parsing).

Notation subcarry := subcarry (only parsing).

Notation addc_def := addc_def (only parsing).
Notation addc := addc (only parsing).

Notation addcarryc_def := addcarryc_def (only parsing).
Notation addcarryc := addcarryc (only parsing).

Notation subc_def := subc_def (only parsing).
Notation subc := subc (only parsing).

Notation subcarryc_def := subcarryc_def (only parsing).
Notation subcarryc := subcarryc (only parsing).

#[deprecated(since="8.14",note="Use Uint63.diveucl_def instead")]
Notation diveucl_def := diveucl_def (only parsing).
#[deprecated(since="8.14",note="Use Uint63.diveucl instead")]
Notation diveucl := diveucl (only parsing).

#[deprecated(since="8.14",note="Use Uint63.diveucl_21 instead")]
Notation diveucl_21 := diveucl_21 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.addmuldiv_def instead")]
Notation addmuldiv_def := addmuldiv_def (only parsing).
#[deprecated(since="8.14",note="Use Uint63.addmuldiv instead")]
Notation addmuldiv := addmuldiv (only parsing).

Module Import Int63NotationsInternalC.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Notation "- x" := (Uint63.opp x) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Notation "n '+c' m" := (Uint63.addc n m) (at level 50, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Notation "n '-c' m" := (Uint63.subc n m) (at level 50, no associativity) : int63_scope.
End Int63NotationsInternalC.

Notation oppc := oppc (only parsing).

Notation succc := succc (only parsing).

Notation predc := predc (only parsing).

#[deprecated(since="8.14",note="Use Uint63.compare_def instead")]
Notation compare_def := compare_def (only parsing).
#[deprecated(since="8.14",note="Use Uint63.compare instead")]
Notation compare := compare (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_rec instead")]
Notation to_Z_rec := to_Z_rec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z instead")]
Notation to_Z := to_Z (only parsing).

#[deprecated(since="8.14",note="Use Uint63.of_pos_rec instead")]
Notation of_pos_rec := of_pos_rec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.of_pos instead")]
Notation of_pos := of_pos (only parsing).

#[deprecated(since="8.14",note="Use Uint63.of_Z instead")]
Notation of_Z := of_Z (only parsing).

Notation wB := wB (only parsing).

Module Import Int63NotationsInternalD.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Notation "n ?= m" := (Uint63.compare n m) (at level 70, no associativity) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Notation "'φ' x" := (Uint63.to_Z x) (at level 0) : int63_scope.
#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Notation "'Φ' x" :=
   (zn2z_to_Z Uint63.wB Uint63.to_Z x) (at level 0) : int63_scope.
End Int63NotationsInternalD.

#[deprecated(since="8.14",note="Use Uint63.to_Z_rec_bounded instead")]
Notation to_Z_rec_bounded := to_Z_rec_bounded (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_bounded instead")]
Notation to_Z_bounded := to_Z_bounded (only parsing).

#[deprecated(since="8.14",note="Use BinInt.Z.div_lt_upper_bound instead")]
Notation Z_lt_div2 := Deprecated.Z_lt_div2 (only parsing).

Require Import ZArith.

#[deprecated(since="8.14",note="Use BinInt.Z.mod_bound_pos_le instead")]
Notation Zmod_le_first := Z.mod_bound_pos_le (only parsing).

#[deprecated(since="8.14",note="Use Uint63.Zmod_distr instead")]
Notation Zmod_distr := Zmod_distr (only parsing).

#[deprecated(since="8.14",note="Use Uint63.pow2_pos instead")]
Notation pow2_pos := pow2_pos (only parsing).

#[deprecated(since="8.14",note="Use Uint63.pow2_nz instead")]
Notation pow2_nz := pow2_nz (only parsing).

Notation wB_diff_0 := wB_diff_0 (only parsing).

Notation wB_pos := wB_pos (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_0 instead")]
Notation to_Z_0 := to_Z_0 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_1 instead")]
Notation to_Z_1 := to_Z_1 (only parsing).

Local Open Scope Z_scope.

#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Local Notation "[+| c |]" := (interp_carry 1 Uint63.wB Uint63.to_Z c)
  (at level 0, c at level 99) : int63_scope.

#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Local Notation "[-| c |]" := (interp_carry (-1) Uint63.wB Uint63.to_Z c)
  (at level 0, c at level 99) : int63_scope.

#[deprecated(since="8.14",note="Use Uint63.of_to_Z instead")]
Notation of_to_Z := of_to_Z (only parsing).

#[deprecated(since="8.14",note="Use Uint63.can_inj instead")]
Notation can_inj := can_inj (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_inj instead")]
Notation to_Z_inj := to_Z_inj (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lsl_spec instead")]
Notation lsl_spec := lsl_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lsr_spec instead")]
Notation lsr_spec := lsr_spec (only parsing).

Notation land_spec := land_spec (only parsing).

Notation lor_spec := lor_spec (only parsing).

Notation lxor_spec := lxor_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.add_spec instead")]
Notation add_spec := add_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sub_spec instead")]
Notation sub_spec := sub_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.mul_spec instead")]
Notation mul_spec := mul_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.mulc_spec instead")]
Notation mulc_spec := mulc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.div_spec instead")]
Notation div_spec := div_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.mod_spec instead")]
Notation mod_spec := mod_spec (only parsing).

Notation eqb_correct := eqb_correct (only parsing).

Notation eqb_refl := eqb_refl (only parsing).

#[deprecated(since="8.14",note="Use Uint63.ltb_spec instead")]
Notation ltb_spec := ltb_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.leb_spec instead")]
Notation leb_spec := leb_spec (only parsing).

Notation head0 := head0 (only parsing).
Notation tail0 := tail0 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.compare_def_spec instead")]
Notation compare_def_spec := compare_def_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.head0_spec instead")]
Notation head0_spec := head0_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.tail0_spec instead")]
Notation tail0_spec := tail0_spec (only parsing).

Notation addc_def_spec := addc_def_spec (only parsing).

Notation addcarryc_def_spec := addcarryc_def_spec (only parsing).

Notation subc_def_spec := subc_def_spec (only parsing).

Notation subcarryc_def_spec := subcarryc_def_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.diveucl_def_spec instead")]
Notation diveucl_def_spec := diveucl_def_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.diveucl_21_spec instead")]
Notation diveucl_21_spec := diveucl_21_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.addmuldiv_def_spec instead")]
Notation addmuldiv_def_spec := addmuldiv_def_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_step instead")]
Notation sqrt_step := sqrt_step (only parsing).

#[deprecated(since="8.14",note="Use Uint63.iter_sqrt instead")]
Notation iter_sqrt := iter_sqrt (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt instead")]
Notation sqrt := sqrt (only parsing).

Notation high_bit := high_bit (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt2_step instead")]
Notation sqrt2_step := sqrt2_step (only parsing).

#[deprecated(since="8.14",note="Use Uint63.iter2_sqrt instead")]
Notation iter2_sqrt := iter2_sqrt (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt2 instead")]
Notation sqrt2 := sqrt2 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.gcd_rec instead")]
Notation gcd_rec := gcd_rec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.gcd instead")]
Notation gcd := gcd (only parsing).

Notation eqb_complete := eqb_complete (only parsing).

Notation eqb_spec := eqb_spec (only parsing).

Notation eqb_false_spec := eqb_false_spec (only parsing).

Notation eqb_false_complete := eqb_false_complete (only parsing).

Notation eqb_false_correct := eqb_false_correct (only parsing).

Notation eqs := eqs (only parsing).

Notation eq_dec := eq_dec (only parsing).

Notation cast := cast (only parsing).

Notation cast_refl := cast_refl (only parsing).

Notation cast_diff := cast_diff (only parsing).

Notation eqo := eqo (only parsing).

Notation eqo_refl := eqo_refl (only parsing).

Notation eqo_diff := eqo_diff (only parsing).

#[deprecated(since="8.14",note="Use Uint63.eqbP instead")]
Notation eqbP := eqbP (only parsing).

#[deprecated(since="8.14",note="Use Uint63.ltbP instead")]
Notation ltbP := ltbP (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lebP instead")]
Notation lebP := lebP (only parsing).

#[deprecated(since="8.14",note="Use Uint63.compare_spec instead")]
Notation compare_spec := compare_spec (only parsing).

Notation is_zero_spec := is_zero_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.diveucl_spec instead")]
Notation diveucl_spec := diveucl_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.addc_spec instead")]
Notation addc_spec := addc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.succ_spec instead")]
Notation succ_spec := succ_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.succc_spec instead")]
Notation succc_spec := succc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.addcarry_spec instead")]
Notation addcarry_spec := addcarry_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.addcarryc_spec instead")]
Notation addcarryc_spec := addcarryc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.subc_spec instead")]
Notation subc_spec := subc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.pred_spec instead")]
Notation pred_spec := pred_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.predc_spec instead")]
Notation predc_spec := predc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.oppc_spec instead")]
Notation oppc_spec := oppc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.opp_spec instead")]
Notation opp_spec := opp_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.oppcarry_spec instead")]
Notation oppcarry_spec := oppcarry_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.subcarry_spec instead")]
Notation subcarry_spec := subcarry_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.subcarryc_spec instead")]
Notation subcarryc_spec := subcarryc_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_gcd instead")]
Notation to_Z_gcd := to_Z_gcd (only parsing).

#[deprecated(since="8.14",note="Use Uint63.gcd_spec instead")]
Notation gcd_spec := gcd_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.head00_spec instead")]
Notation head00_spec := head00_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.tail00_spec instead")]
Notation tail00_spec := tail00_spec (only parsing).

#[deprecated(since="8.14",note="Use the uint63_scope instead.")]
Infix "≡" := (eqm Uint63.wB) (at level 70, no associativity) : int63_scope.

Notation eqm_mod := eqm_mod (only parsing).

Notation eqm_sub := eqm_sub (only parsing).

Notation eqmE := eqmE (only parsing).

Notation eqm_subE := eqm_subE (only parsing).

#[deprecated(since="8.14",note="Use Uint63.int_eqm instead")]
Notation int_eqm := int_eqm (only parsing).

#[deprecated(since="8.14",note="Use Uint63.eqmI instead")]
Notation eqmI := eqmI (only parsing).

Notation add_assoc := add_assoc (only parsing).

Notation add_comm := add_comm (only parsing).

#[deprecated(since="8.14",note="Use Uint63.add_le_r instead")]
Notation add_le_r := add_le_r (only parsing).

Notation add_cancel_l := add_cancel_l (only parsing).

Notation add_cancel_r := add_cancel_r (only parsing).

Notation b2i := b2i (only parsing).

Notation lsr0 := lsr0 (only parsing).

Notation lsr_0_r := lsr_0_r (only parsing).

Notation lsr_1 := lsr_1 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lsr_add instead")]
Notation lsr_add := lsr_add (only parsing).

Notation lsl0 := lsl0 (only parsing).

Notation lsl0_r := lsl0_r (only parsing).

Notation lsl_add_distr := lsl_add_distr (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lsr_M_r instead")]
Notation lsr_M_r := lsr_M_r (only parsing).

#[deprecated(since="8.14",note="Use Uint63.bit_0_spec instead")]
Notation bit_0_spec := bit_0_spec (only parsing).

Notation bit_split := bit_split (only parsing).

#[deprecated(since="8.14",note="Use Uint63.bit_lsr instead")]
Notation bit_lsr := bit_lsr (only parsing).

Notation bit_b2i := bit_b2i (only parsing).

Notation bit_1 := bit_1 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.to_Z_split instead")]
Notation to_Z_split := to_Z_split (only parsing).

#[deprecated(since="8.14",note="Use Uint63.bit_M instead")]
Notation bit_M := bit_M (only parsing).

#[deprecated(since="8.14",note="Use Uint63.bit_half instead")]
Notation bit_half := bit_half (only parsing).

Notation bit_ext := bit_ext (only parsing).

#[deprecated(since="8.14",note="Use Uint63.bit_lsl instead")]
Notation bit_lsl := bit_lsl (only parsing).

Notation lor_lsr := lor_lsr (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lor_le instead")]
Notation lor_le := lor_le (only parsing).

Notation bit_0 := bit_0 (only parsing).

Notation bit_add_or := bit_add_or (only parsing).

#[deprecated(since="8.14",note="Use Uint63.addmuldiv_spec instead")]
Notation addmuldiv_spec := addmuldiv_spec (only parsing).

Notation is_even_bit := is_even_bit (only parsing).

#[deprecated(since="8.14",note="Use Uint63.is_even_spec instead")]
Notation is_even_spec := is_even_spec (only parsing).

Notation is_even_0 := is_even_0 (only parsing).

Notation is_even_lsl_1 := is_even_lsl_1 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.elim_div instead")]
Ltac elim_div := elim_div.

#[deprecated(since="8.14",note="Use Uint63.quotient_by_2 instead")]
Notation quotient_by_2 := quotient_by_2 (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_main_trick instead")]
Notation sqrt_main_trick := sqrt_main_trick (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_main instead")]
Notation sqrt_main := sqrt_main (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_test_false instead")]
Notation sqrt_test_false := sqrt_test_false (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_test_true instead")]
Notation sqrt_test_true := sqrt_test_true (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_step_correct instead")]
Notation sqrt_step_correct := sqrt_step_correct (only parsing).

#[deprecated(since="8.14",note="Use Uint63.iter_sqrt_correct instead")]
Notation iter_sqrt_correct := iter_sqrt_correct (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_init instead")]
Notation sqrt_init := sqrt_init (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt_spec instead")]
Notation sqrt_spec := sqrt_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt2_step_def instead")]
Notation sqrt2_step_def := sqrt2_step_def (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt2_lower_bound instead")]
Notation sqrt2_lower_bound := sqrt2_lower_bound (only parsing).

#[deprecated(since="8.14",note="Use Uint63.diveucl_21_spec_aux instead")]
Notation diveucl_21_spec_aux := diveucl_21_spec_aux (only parsing).

#[deprecated(since="8.14",note="Use Uint63.div2_phi instead")]
Notation div2_phi := div2_phi (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt2_step_correct instead")]
Notation sqrt2_step_correct := sqrt2_step_correct (only parsing).

#[deprecated(since="8.14",note="Use Uint63.iter2_sqrt_correct instead")]
Notation iter2_sqrt_correct := iter2_sqrt_correct (only parsing).

#[deprecated(since="8.14",note="Use Uint63.sqrt2_spec instead")]
Notation sqrt2_spec := sqrt2_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.of_pos_rec_spec instead")]
Notation of_pos_rec_spec := of_pos_rec_spec (only parsing).

#[deprecated(since="8.14",note="Use Uint63.is_int instead")]
Notation is_int := is_int (only parsing).

#[deprecated(since="8.14",note="Use Uint63.of_Z_spec instead")]
Notation of_Z_spec := of_Z_spec (only parsing).

#[deprecated(since="8.14",note="Use Bool.negb_sym instead")]
Notation negbE := Deprecated.negbE (only parsing).

#[deprecated(since="8.14",note="Use Uint63.Z_oddE instead")]
Notation Z_oddE := Z_oddE (only parsing).

#[deprecated(since="8.14",note="Use Uint63.Z_evenE instead")]
Notation Z_evenE := Z_evenE (only parsing).

#[deprecated(since="8.14",note="Use Uint63.is_zeroE instead")]
Notation is_zeroE := is_zeroE (only parsing).

#[deprecated(since="8.14",note="Use Uint63.bitE instead")]
Notation bitE := bitE (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lt_pow_lt_log instead")]
Notation lt_pow_lt_log := lt_pow_lt_log (only parsing).

#[deprecated(since="8.14",note="Use Uint63.land_spec' instead")]
Notation land_spec' := land_spec' (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lor_spec' instead")]
Notation lor_spec' := lor_spec' (only parsing).

#[deprecated(since="8.14",note="Use Uint63.lxor_spec' instead")]
Notation lxor_spec' := lxor_spec' (only parsing).

Notation landC := landC (only parsing).

Notation landA := landA (only parsing).

Notation land0 := land0 (only parsing).

Notation land0_r := land0_r (only parsing).

Notation lorC := lorC (only parsing).

Notation lorA := lorA (only parsing).

Notation lor0 := lor0 (only parsing).

Notation lor0_r := lor0_r (only parsing).

Notation lxorC := lxorC (only parsing).

Notation lxorA := lxorA (only parsing).

Notation lxor0 := lxor0 (only parsing).

Notation lxor0_r := lxor0_r (only parsing).

#[deprecated(since="8.14",note="Use Uint63.opp_to_Z_opp instead")]
Notation opp_to_Z_opp := opp_to_Z_opp (only parsing).

Module Export Int63Notations.
  Local Open Scope uint63_scope.
  #[deprecated(since="8.13",note="use infix mod in the uint63_scope instead")]
   Notation "a \% m" := (a mod m) (at level 40, left associativity) : int63_scope.
  #[deprecated(since="8.13",note="use infix =? in the uint63_scope instead")]
   Notation "m '==' n" := (m =? n) (at level 70, no associativity) : int63_scope.
  #[deprecated(since="8.13",note="use infix <? in the uint63_scope instead")]
   Notation "m < n" := (m <? n) : int63_scope.
  #[deprecated(since="8.13",note="use infix <=? in the uint63_scope instead")]
   Notation "m <= n" := (m <=? n) : int63_scope.
  #[deprecated(since="8.13",note="use infix ≤? in the uint63_scope instead")]
   Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope.
  Export Int63NotationsInternalB.
  Export Int63NotationsInternalC.
  Export Int63NotationsInternalD.
End Int63Notations.