summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3775logplain
-rw-r--r--arguments_renaming.mli995logplain
-rw-r--r--cases.ml73440logplain
-rw-r--r--cases.mli2065logplain
-rw-r--r--cbv.ml14096logplain
-rw-r--r--cbv.mli2071logplain
-rw-r--r--classops.ml13548logplain
-rw-r--r--classops.mli3419logplain
-rw-r--r--coercion.ml10518logplain
-rw-r--r--coercion.mli2897logplain
-rw-r--r--detyping.ml25110logplain
-rw-r--r--detyping.mli2866logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml32570logplain
-rw-r--r--evarconv.mli1951logplain
-rw-r--r--evarutil.ml81102logplain
-rw-r--r--evarutil.mli9276logplain
-rw-r--r--evd.ml30042logplain
-rw-r--r--evd.mli11407logplain
-rw-r--r--glob_term.ml15704logplain
-rw-r--r--glob_term.mli5816logplain
-rw-r--r--indrec.ml19834logplain
-rw-r--r--indrec.mli2379logplain
-rw-r--r--inductiveops.ml16013logplain
-rw-r--r--inductiveops.mli5393logplain
-rw-r--r--matching.ml12667logplain
-rw-r--r--matching.mli3947logplain
-rw-r--r--namegen.ml11652logplain
-rw-r--r--namegen.mli3658logplain
-rw-r--r--pattern.ml13812logplain
-rw-r--r--pattern.mli4770logplain
-rw-r--r--pretype_errors.ml6590logplain
-rw-r--r--pretype_errors.mli4473logplain
-rw-r--r--pretyping.ml29349logplain
-rw-r--r--pretyping.mli4498logplain
-rw-r--r--pretyping.mllib272logplain
-rw-r--r--recordops.ml12854logplain
-rw-r--r--recordops.mli3094logplain
-rw-r--r--reductionops.ml32367logplain
-rw-r--r--reductionops.mli8979logplain
-rw-r--r--retyping.ml7270logplain
-rw-r--r--retyping.mli1694logplain
-rw-r--r--tacred.ml38190logplain
-rw-r--r--tacred.mli3724logplain
-rw-r--r--term_dnet.ml13141logplain
-rw-r--r--term_dnet.mli3448logplain
-rw-r--r--termops.ml38560logplain
-rw-r--r--termops.mli11455logplain
-rw-r--r--typeclasses.ml16011logplain
-rw-r--r--typeclasses.mli4634logplain
-rw-r--r--typeclasses_errors.ml2019logplain
-rw-r--r--typeclasses_errors.mli1492logplain
-rw-r--r--typing.ml10241logplain
-rw-r--r--typing.mli1553logplain
-rw-r--r--unification.ml47604logplain
-rw-r--r--unification.mli2951logplain
-rw-r--r--vnorm.ml10376logplain
-rw-r--r--vnorm.mli655logplain