aboutsummaryrefslogtreecommitdiff
path: root/vernac
ModeNameSize
-rw-r--r--.ocamlformat-enable12logplain
-rw-r--r--assumptions.ml14618logplain
-rw-r--r--assumptions.mli1592logplain
-rw-r--r--attributes.ml7639logplain
-rw-r--r--attributes.mli4925logplain
-rw-r--r--auto_ind_decl.ml44750logplain
-rw-r--r--auto_ind_decl.mli1850logplain
-rw-r--r--canonical.ml2000logplain
-rw-r--r--canonical.mli754logplain
-rw-r--r--classes.ml24054logplain
-rw-r--r--classes.mli2824logplain
-rw-r--r--comArguments.ml12243logplain
-rw-r--r--comArguments.mli916logplain
-rw-r--r--comAssumption.ml11491logplain
-rw-r--r--comAssumption.mli1553logplain
-rw-r--r--comCoercion.ml12807logplain
-rw-r--r--comCoercion.mli2184logplain
-rw-r--r--comDefinition.ml5818logplain
-rw-r--r--comDefinition.mli1298logplain
-rw-r--r--comFixpoint.ml15374logplain
-rw-r--r--comFixpoint.mli2726logplain
-rw-r--r--comHints.ml5785logplain
-rw-r--r--comHints.mli751logplain
-rw-r--r--comInductive.ml26559logplain
-rw-r--r--comInductive.mli3780logplain
-rw-r--r--comPrimitive.ml1856logplain
-rw-r--r--comPrimitive.mli775logplain
-rw-r--r--comProgramFixpoint.ml16876logplain
-rw-r--r--comProgramFixpoint.mli1007logplain
-rw-r--r--declare.ml41658logplain
-rw-r--r--declare.mli13351logplain
-rw-r--r--declareDef.ml398logplain
-rw-r--r--declareInd.ml7649logplain
-rw-r--r--declareInd.mli1314logplain
-rw-r--r--declareObl.ml20784logplain
-rw-r--r--declareObl.mli4841logplain
-rw-r--r--declareUniv.ml4914logplain
-rw-r--r--declareUniv.mli1018logplain
-rw-r--r--declaremods.ml38560logplain
-rw-r--r--declaremods.mli4275logplain
-rw-r--r--doc.tex246logplain
-rw-r--r--dune175logplain
-rw-r--r--egramcoq.ml24886logplain
-rw-r--r--egramcoq.mli1174logplain
-rw-r--r--egramml.ml3447logplain
-rw-r--r--egramml.mli1534logplain
-rw-r--r--g_proofs.mlg6206logplain
-rw-r--r--g_vernac.mlg47140logplain
-rw-r--r--himsg.ml59703logplain
-rw-r--r--himsg.mli1042logplain
-rw-r--r--indschemes.ml20714logplain
-rw-r--r--indschemes.mli2042logplain
-rw-r--r--lemmas.ml17390logplain
-rw-r--r--lemmas.mli3518logplain
-rw-r--r--library.ml19191logplain
-rw-r--r--library.mli3157logplain
-rw-r--r--loadpath.ml9731logplain
-rw-r--r--loadpath.mli2709logplain
-rw-r--r--locality.ml3427logplain
-rw-r--r--locality.mli1933logplain
-rw-r--r--metasyntax.ml74161logplain
-rw-r--r--metasyntax.mli2490logplain
-rw-r--r--mltop.ml13004logplain
-rw-r--r--mltop.mli2637logplain
-rw-r--r--obligations.ml15432logplain
-rw-r--r--obligations.mli5742logplain
-rw-r--r--pfedit.ml766logplain
-rw-r--r--ppvernac.ml50937logplain
-rw-r--r--ppvernac.mli1258logplain
-rw-r--r--prettyp.ml39623logplain
-rw-r--r--prettyp.mli4789logplain
-rw-r--r--proof_global.ml487logplain
-rw-r--r--proof_using.ml6631logplain
-rw-r--r--proof_using.mli1184logplain
-rw-r--r--pvernac.ml2968logplain
-rw-r--r--pvernac.mli2138logplain
-rw-r--r--recLemmas.ml4782logplain
-rw-r--r--recLemmas.mli869logplain
-rw-r--r--record.ml31649logplain
-rw-r--r--record.mli1549logplain
-rw-r--r--retrieveObl.ml10222logplain
-rw-r--r--retrieveObl.mli1899logplain
-rw-r--r--search.ml13722logplain
-rw-r--r--search.mli3529logplain
-rw-r--r--topfmt.ml15152logplain
-rw-r--r--topfmt.mli2577logplain
-rw-r--r--vernac.mllib527logplain
-rw-r--r--vernacentries.ml87533logplain
-rw-r--r--vernacentries.mli1285logplain
-rw-r--r--vernacexpr.ml16803logplain
-rw-r--r--vernacextend.ml9405logplain
-rw-r--r--vernacextend.mli4863logplain
-rw-r--r--vernacinterp.ml10832logplain
-rw-r--r--vernacinterp.mli1557logplain
-rw-r--r--vernacprop.ml1424logplain
-rw-r--r--vernacprop.mli987logplain
-rw-r--r--vernacstate.ml5614logplain
-rw-r--r--vernacstate.mli3135logplain
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 01:07:16 +0000