Code

Replace deprecated proof components#185

Code

Merged

spitters merged 6 commits intocoq-community:mastercoq-community/corn:masterfrom anandadalton:lt_le_transanandadalton/corn:lt_le_transCopy head branch name to clipboardMay 16, 2023

+664-665

Commits

Commits on May 15, 2023

• Replace deprecated le_refl with Nat.le_refl

  anandadalton

  committed
  7c5bfc3

  Copy full SHA for 7c5bfc3

• Change deprecated "lt_le_weak" -> "Nat.lt_le_incl"

  anandadalton

  committed
  9d468a7

  Copy full SHA for 9d468a7

• Deprecated lt_n_Sn changes to Nat.lt_succ_diag_r

  anandadalton

  committed
  8176f3d

  Copy full SHA for 8176f3d

• Deprecated lt_S becomes Nat.lt_lt_succ_r

  anandadalton

  committed
  95dbc0c

  Copy full SHA for 95dbc0c

• Deprecate le_O_n and replace with Nat.le_0_l.

  anandadalton

  committed
  b974323

  Copy full SHA for b974323

• Replace deprecated lt_irrefl with Nat.lt_irrefl

  anandadalton

  committed
  22d7888

  Copy full SHA for 22d7888