aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
ModeNameSize
-rw-r--r--assumptions.ml14346logplain
-rw-r--r--assumptions.mli1438logplain
-rw-r--r--auto_ind_decl.ml41162logplain
-rw-r--r--auto_ind_decl.mli1610logplain
-rw-r--r--class.ml10504logplain
-rw-r--r--class.mli2189logplain
-rw-r--r--classes.ml17108logplain
-rw-r--r--classes.mli2180logplain
-rw-r--r--command.ml55627logplain
-rw-r--r--command.mli6255logplain
-rw-r--r--declareDef.ml2544logplain
-rw-r--r--declareDef.mli1141logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--explainErr.ml4991logplain
-rw-r--r--explainErr.mli983logplain
-rw-r--r--himsg.ml55797logplain
-rw-r--r--himsg.mli1599logplain
-rw-r--r--indschemes.ml19141logplain
-rw-r--r--indschemes.mli1656logplain
-rw-r--r--lemmas.ml22023logplain
-rw-r--r--lemmas.mli3069logplain
-rw-r--r--locality.ml3225logplain
-rw-r--r--locality.mli1937logplain
-rw-r--r--metasyntax.ml57630logplain
-rw-r--r--metasyntax.mli2246logplain
-rw-r--r--mltop.ml15617logplain
-rw-r--r--mltop.mli3065logplain
-rw-r--r--obligations.ml42931logplain
-rw-r--r--obligations.mli4511logplain
-rw-r--r--proof_using.ml6864logplain
-rw-r--r--proof_using.mli975logplain
-rw-r--r--record.ml25986logplain
-rw-r--r--record.mli982logplain
-rw-r--r--search.ml13083logplain
-rw-r--r--search.mli3314logplain
-rw-r--r--topfmt.ml10719logplain
-rw-r--r--topfmt.mli2085logplain
-rw-r--r--vernac.mllib215logplain
-rw-r--r--vernacentries.ml87096logplain
-rw-r--r--vernacentries.mli1579logplain
-rw-r--r--vernacinterp.ml2559logplain
-rw-r--r--vernacinterp.mli1117logplain
-rw-r--r--vernacprop.ml1721logplain
-rw-r--r--vernacprop.mli885logplain
-rw-r--r--vernacstate.ml1332logplain
-rw-r--r--vernacstate.mli914logplain