Code

Remove deprecated options/flags#198

Code

Merged

spitters merged 1 commit intocoq-community:mastercoq-community/corn:masterfrom anandadalton:deprecationsanandadalton/corn:deprecationsCopy head branch name to clipboardMay 31, 2023

-34

Commits

Commits on May 31, 2023

• 'remove deprecated options/flags'

  anandadalton

  committed
  cba97fd

  Copy full SHA for cba97fd