aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
ModeNameSize
-rw-r--r--assumptions.ml14472logplain
-rw-r--r--assumptions.mli1439logplain
-rw-r--r--auto_ind_decl.ml40606logplain
-rw-r--r--auto_ind_decl.mli1610logplain
-rw-r--r--class.ml10298logplain
-rw-r--r--class.mli2189logplain
-rw-r--r--classes.ml16782logplain
-rw-r--r--classes.mli2172logplain
-rw-r--r--command.ml54546logplain
-rw-r--r--command.mli6184logplain
-rw-r--r--declareDef.ml2547logplain
-rw-r--r--declareDef.mli1124logplain
-rw-r--r--discharge.ml4438logplain
-rw-r--r--discharge.mli680logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--explainErr.ml4929logplain
-rw-r--r--explainErr.mli983logplain
-rw-r--r--himsg.ml56358logplain
-rw-r--r--himsg.mli1576logplain
-rw-r--r--indschemes.ml19114logplain
-rw-r--r--indschemes.mli1688logplain
-rw-r--r--lemmas.ml21381logplain
-rw-r--r--lemmas.mli3081logplain
-rw-r--r--locality.ml3718logplain
-rw-r--r--locality.mli2212logplain
-rw-r--r--metasyntax.ml55696logplain
-rw-r--r--metasyntax.mli2198logplain
-rw-r--r--mltop.ml15577logplain
-rw-r--r--mltop.mli3065logplain
-rw-r--r--obligations.ml41676logplain
-rw-r--r--obligations.mli4587logplain
-rw-r--r--record.ml25227logplain
-rw-r--r--record.mli1918logplain
-rw-r--r--search.ml13081logplain
-rw-r--r--search.mli3312logplain
-rw-r--r--topfmt.ml10689logplain
-rw-r--r--topfmt.mli2085logplain
-rw-r--r--vernac.mllib191logplain
-rw-r--r--vernacentries.ml84708logplain
-rw-r--r--vernacentries.mli1439logplain
-rw-r--r--vernacinterp.ml2484logplain
-rw-r--r--vernacinterp.mli966logplain
-rw-r--r--vernacprop.ml1737logplain
-rw-r--r--vernacprop.mli885logplain