aboutsummaryrefslogtreecommitdiff
path: root/theories/funind
ModeNameSize
-rw-r--r--FunInd.v746logplain
-rw-r--r--Recdef.v1648logplain