aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
ModeNameSize
-rw-r--r--assumptions.ml14304logplain
-rw-r--r--assumptions.mli1439logplain
-rw-r--r--auto_ind_decl.ml40711logplain
-rw-r--r--auto_ind_decl.mli1610logplain
-rw-r--r--class.ml10342logplain
-rw-r--r--class.mli2189logplain
-rw-r--r--classes.ml16772logplain
-rw-r--r--classes.mli2178logplain
-rw-r--r--command.ml54777logplain
-rw-r--r--command.mli6330logplain
-rw-r--r--declareDef.ml2547logplain
-rw-r--r--declareDef.mli1124logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--explainErr.ml4929logplain
-rw-r--r--explainErr.mli983logplain
-rw-r--r--himsg.ml55533logplain
-rw-r--r--himsg.mli1576logplain
-rw-r--r--indschemes.ml19144logplain
-rw-r--r--indschemes.mli1676logplain
-rw-r--r--lemmas.ml21613logplain
-rw-r--r--lemmas.mli3055logplain
-rw-r--r--locality.ml3718logplain
-rw-r--r--locality.mli2212logplain
-rw-r--r--metasyntax.ml57609logplain
-rw-r--r--metasyntax.mli2246logplain
-rw-r--r--mltop.ml15617logplain
-rw-r--r--mltop.mli3065logplain
-rw-r--r--obligations.ml41834logplain
-rw-r--r--obligations.mli4631logplain
-rw-r--r--proof_using.ml6864logplain
-rw-r--r--proof_using.mli975logplain
-rw-r--r--record.ml25365logplain
-rw-r--r--record.mli1921logplain
-rw-r--r--search.ml13081logplain
-rw-r--r--search.mli3312logplain
-rw-r--r--topfmt.ml10719logplain
-rw-r--r--topfmt.mli2085logplain
-rw-r--r--vernac.mllib203logplain
-rw-r--r--vernacentries.ml87014logplain
-rw-r--r--vernacentries.mli1944logplain
-rw-r--r--vernacinterp.ml2484logplain
-rw-r--r--vernacinterp.mli966logplain
-rw-r--r--vernacprop.ml1721logplain
-rw-r--r--vernacprop.mli885logplain