aboutsummaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--astterm.ml22385logplain
-rwxr-xr-xastterm.mli819logplain
-rw-r--r--class.mli12logplain
-rw-r--r--evarconv.mli12logplain
-rw-r--r--evarutil.mli12logplain
-rw-r--r--multcase.mli12logplain
-rw-r--r--pretyping.mli12logplain
-rw-r--r--rawterm.ml1622logplain
-rw-r--r--record.mli12logplain