Moving closed notations at level 0 in anticipation of the removal of the Coq fallback ignoring levels when nothing else applies.#134

Merged

jwiegley merged 2 commits intojwiegley:masterfrom herbelin:master+closed-notation-level-0

Nov 6, 2023

+27-27

Commits on Oct 29, 2023

Moving closed notations at level 0 in anticipation of removing Coq's
herbelin
committed
Extra parentheses needed in argument of a prefix notation at level 0.
herbelin
committed