summaryrefslogtreecommitdiff
path: root/vernac
ModeNameSize
-rw-r--r--assumptions.ml14391logplain
-rw-r--r--assumptions.mli1588logplain
-rw-r--r--auto_ind_decl.ml41531logplain
-rw-r--r--auto_ind_decl.mli1760logplain
-rw-r--r--class.ml10646logplain
-rw-r--r--class.mli2339logplain
-rw-r--r--classes.ml17830logplain
-rw-r--r--classes.mli2353logplain
-rw-r--r--comAssumption.ml7230logplain
-rw-r--r--comAssumption.mli1564logplain
-rw-r--r--comDefinition.ml5599logplain
-rw-r--r--comDefinition.mli1488logplain
-rw-r--r--comFixpoint.ml14738logplain
-rw-r--r--comFixpoint.mli3610logplain
-rw-r--r--comInductive.ml18375logplain
-rw-r--r--comInductive.mli2515logplain
-rw-r--r--comProgramFixpoint.ml14880logplain
-rw-r--r--comProgramFixpoint.mli369logplain
-rw-r--r--declareDef.ml2738logplain
-rw-r--r--declareDef.mli1291logplain
-rw-r--r--explainErr.ml5187logplain
-rw-r--r--explainErr.mli1133logplain
-rw-r--r--himsg.ml55839logplain
-rw-r--r--himsg.mli1749logplain
-rw-r--r--indschemes.ml19002logplain
-rw-r--r--indschemes.mli2082logplain
-rw-r--r--lemmas.ml21873logplain
-rw-r--r--lemmas.mli3263logplain
-rw-r--r--locality.ml2669logplain
-rw-r--r--locality.mli1936logplain
-rw-r--r--metasyntax.ml60592logplain
-rw-r--r--metasyntax.mli2293logplain
-rw-r--r--mltop.ml16285logplain
-rw-r--r--mltop.mli3551logplain
-rw-r--r--obligations.ml43080logplain
-rw-r--r--obligations.mli4747logplain
-rw-r--r--proof_using.ml7023logplain
-rw-r--r--proof_using.mli1125logplain
-rw-r--r--record.ml25346logplain
-rw-r--r--record.mli1420logplain
-rw-r--r--search.ml13233logplain
-rw-r--r--search.mli3464logplain
-rw-r--r--topfmt.ml11058logplain
-rw-r--r--topfmt.mli2237logplain
-rw-r--r--vernac.mllib279logplain
-rw-r--r--vernacentries.ml89773logplain
-rw-r--r--vernacentries.mli1783logplain
-rw-r--r--vernacinterp.ml2742logplain
-rw-r--r--vernacinterp.mli1306logplain
-rw-r--r--vernacprop.ml2128logplain
-rw-r--r--vernacprop.mli1330logplain
-rw-r--r--vernacstate.ml1550logplain
-rw-r--r--vernacstate.mli1064logplain