aboutsummaryrefslogtreecommitdiff
path: root/library
ModeNameSize
-rw-r--r--coqlib.ml10987logplain
-rw-r--r--coqlib.mli10617logplain
-rw-r--r--doc.tex512logplain
-rw-r--r--dune174logplain
-rw-r--r--global.ml8506logplain
-rw-r--r--global.mli6789logplain
-rw-r--r--globnames.ml4495logplain
-rw-r--r--globnames.mli2807logplain
-rw-r--r--goptions.ml17295logplain
-rw-r--r--goptions.mli8286logplain
-rw-r--r--lib.ml19036logplain
-rw-r--r--lib.mli6633logplain
-rw-r--r--libnames.ml4729logplain
-rw-r--r--libnames.mli3508logplain
-rw-r--r--libobject.ml6470logplain
-rw-r--r--libobject.mli7360logplain
-rw-r--r--library.mllib72logplain
-rw-r--r--nametab.ml18383logplain
-rw-r--r--nametab.mli8703logplain
-rw-r--r--summary.ml5246logplain
-rw-r--r--summary.mli3863logplain