Code

Deprecated notations#194

Code

Merged

spitters merged 12 commits intocoq-community:mastercoq-community/corn:masterfrom anandadalton:easy_fixesanandadalton/corn:easy_fixesCopy head branch name to clipboardMay 24, 2023

+89-85

Commits

Commits on May 22, 2023

• 'Deprecate le_plus_minus for Nat.sub_add'

  anandadalton

  committed
  7763ce1

  Copy full SHA for 7763ce1

Commits on May 24, 2023

• 'Deprecate neq_O_lt for Nat.neq_0_lt_0'

  anandadalton

  committed
  024db94

  Copy full SHA for 024db94

• 'Deprecate le_n_O_eq for Nat.le_0_r'

  anandadalton

  committed
  5b31252

  Copy full SHA for 5b31252

• 'Deprecate le_Sn_le for Nat.lt_le_incl'

  anandadalton

  committed
  6521bf9

  Copy full SHA for 6521bf9

• 'Deprecate Zdiv_eucl_POS for Coq.ZArith.BinIntDef.Z.pos_div_eucl'

  anandadalton

  committed
  aa3859d

  Copy full SHA for aa3859d

• 'Deprecate lt_S_n for Nat.succ_lt_mono'

  anandadalton

  committed
  7a5dc70

  Copy full SHA for 7a5dc70

• 'Deprecate minus_n_n for Nat.sub_diag'

  anandadalton

  committed
  f41ab4f

  Copy full SHA for f41ab4f

• 'Deprecate le_lt_n_Sm for Nat.lt_succ_r'

  anandadalton

  committed
  5735f42

  Copy full SHA for 5735f42

• 'Deprecate Nat.mod_add for Nat.Div0.mod_add'

  anandadalton

  committed
  7e39c78

  Copy full SHA for 7e39c78

• 'Deprecate lt_O_neq for Nat.neq_0_lt_0'

  anandadalton

  committed
  e28ce44

  Copy full SHA for e28ce44

• 'Deprecate lt_le_S for Nat.le_succ_l'

  anandadalton

  committed
  e275fc7

  Copy full SHA for e275fc7

• Merge branch 'coq-community:master' into easy_fixes

  anandadalton

  authored
  2a7c386

  Copy full SHA for 2a7c386