fix notation warnings in 8.20

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.23k stars 185 forks source link

fix notation warnings in 8.20 #1972

Closed Alizter closed 1 month ago

Alizter commented 1 month ago

Newer versions of Coq warn when a postfix or a closed notation doesn't have level 1 or 0 respectively. We fix all such occurences here. We also remove a few redundant reservations.