Skip to content

[WIP]removed deprecation warnings and most duplicate clear warnings#41

Open
ybertot wants to merge 2 commits intocoq-community:masterfrom ybertot:rm-depr-mc14
+124-98

Commits

Commits on Mar 13, 2022

Commits on Mar 14, 2022