summaryrefslogtreecommitdiff
path: root/library
ModeNameSize
-rw-r--r--declare.ml17351logplain
-rw-r--r--declare.mli3702logplain
-rw-r--r--declaremods.ml32202logplain
-rw-r--r--declaremods.mli3908logplain
-rw-r--r--decls.ml2365logplain
-rw-r--r--decls.mli1750logplain
-rw-r--r--dischargedhypsmap.ml851logplain
-rw-r--r--dischargedhypsmap.mli821logplain
-rw-r--r--doc.tex512logplain
-rw-r--r--global.ml9700logplain
-rw-r--r--global.mli6367logplain
-rw-r--r--globnames.ml8302logplain
-rw-r--r--globnames.mli3516logplain
-rw-r--r--goptions.ml13206logplain
-rw-r--r--goptions.mli6457logplain
-rw-r--r--heads.ml6344logplain
-rw-r--r--heads.mli1095logplain
-rw-r--r--impargs.ml26258logplain
-rw-r--r--impargs.mli5931logplain
-rw-r--r--keys.ml4320logplain
-rw-r--r--keys.mli895logplain
-rw-r--r--kindops.ml2077logplain
-rw-r--r--kindops.mli773logplain
-rw-r--r--lib.ml21194logplain
-rw-r--r--lib.mli7565logplain
-rw-r--r--libnames.ml6717logplain
-rw-r--r--libnames.mli4516logplain
-rw-r--r--libobject.ml5994logplain
-rw-r--r--libobject.mli4406logplain
-rw-r--r--library.ml29238logplain
-rw-r--r--library.mli3555logplain
-rw-r--r--library.mllib162logplain
-rw-r--r--loadpath.ml3954logplain
-rw-r--r--loadpath.mli2166logplain
-rw-r--r--nameops.ml4291logplain
-rw-r--r--nameops.mli1990logplain
-rw-r--r--nametab.ml16552logplain
-rw-r--r--nametab.mli6713logplain
-rw-r--r--states.ml1370logplain
-rw-r--r--states.mli1597logplain
-rw-r--r--summary.ml6021logplain
-rw-r--r--summary.mli3298logplain
-rw-r--r--universes.ml37909logplain
-rw-r--r--universes.mli10859logplain