summaryrefslogtreecommitdiff
path: root/vernac
ModeNameSize
-rw-r--r--assumptions.ml14391logplain
-rw-r--r--assumptions.mli1586logplain
-rw-r--r--auto_ind_decl.ml41455logplain
-rw-r--r--auto_ind_decl.mli1743logplain
-rw-r--r--class.ml10807logplain
-rw-r--r--class.mli2293logplain
-rw-r--r--classes.ml18004logplain
-rw-r--r--classes.mli2308logplain
-rw-r--r--comAssumption.ml7231logplain
-rw-r--r--comAssumption.mli1544logplain
-rw-r--r--comDefinition.ml5088logplain
-rw-r--r--comDefinition.mli1485logplain
-rw-r--r--comFixpoint.ml14710logplain
-rw-r--r--comFixpoint.mli3598logplain
-rw-r--r--comInductive.ml22191logplain
-rw-r--r--comInductive.mli2629logplain
-rw-r--r--comProgramFixpoint.ml15072logplain
-rw-r--r--comProgramFixpoint.mli369logplain
-rw-r--r--declareDef.ml2738logplain
-rw-r--r--declareDef.mli1240logplain
-rw-r--r--egramcoq.ml21008logplain
-rw-r--r--egramcoq.mli1131logplain
-rw-r--r--egramml.ml3358logplain
-rw-r--r--egramml.mli1565logplain
-rw-r--r--explainErr.ml5458logplain
-rw-r--r--explainErr.mli1133logplain
-rw-r--r--g_proofs.mlg6221logplain
-rw-r--r--g_vernac.mlg47561logplain
-rw-r--r--himsg.ml56347logplain
-rw-r--r--himsg.mli1962logplain
-rw-r--r--indschemes.ml19007logplain
-rw-r--r--indschemes.mli2042logplain
-rw-r--r--lemmas.ml21605logplain
-rw-r--r--lemmas.mli3220logplain
-rw-r--r--locality.ml2669logplain
-rw-r--r--locality.mli1936logplain
-rw-r--r--metasyntax.ml66009logplain
-rw-r--r--metasyntax.mli2338logplain
-rw-r--r--misctypes.ml4057logplain
-rw-r--r--mltop.ml15924logplain
-rw-r--r--mltop.mli3416logplain
-rw-r--r--obligations.ml43309logplain
-rw-r--r--obligations.mli4699logplain
-rw-r--r--ppvernac.ml47190logplain
-rw-r--r--ppvernac.mli1292logplain
-rw-r--r--proof_using.ml6758logplain
-rw-r--r--proof_using.mli1125logplain
-rw-r--r--pvernac.ml2101logplain
-rw-r--r--pvernac.mli1484logplain
-rw-r--r--record.ml28585logplain
-rw-r--r--record.mli1454logplain
-rw-r--r--search.ml13254logplain
-rw-r--r--search.mli3435logplain
-rw-r--r--topfmt.ml13652logplain
-rw-r--r--topfmt.mli2425logplain
-rw-r--r--vernac.mllib353logplain
-rw-r--r--vernacentries.ml97820logplain
-rw-r--r--vernacentries.mli2955logplain
-rw-r--r--vernacexpr.ml21404logplain
-rw-r--r--vernacinterp.ml3029logplain
-rw-r--r--vernacinterp.mli1622logplain
-rw-r--r--vernacprop.ml2106logplain
-rw-r--r--vernacprop.mli1330logplain
-rw-r--r--vernacstate.ml1550logplain
-rw-r--r--vernacstate.mli1064logplain