aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/prerequisite
ModeNameSize
-rw-r--r--admit.v65logplain
-rw-r--r--bind_univs.v155logplain
-rw-r--r--make_local.v242logplain
-rw-r--r--make_notation.v369logplain
-rw-r--r--ssr_mini_mathcomp.v47522logplain
-rw-r--r--ssr_ssrsyntax1.v1097logplain