aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3611logplain
-rw-r--r--arguments_renaming.mli1003logplain
-rw-r--r--cases.ml96209logplain
-rw-r--r--cases.mli4198logplain
-rw-r--r--cbv.ml14480logplain
-rw-r--r--cbv.mli2150logplain
-rw-r--r--classops.ml17041logplain
-rw-r--r--classops.mli3682logplain
-rw-r--r--coercion.ml17729logplain
-rw-r--r--coercion.mli2935logplain
-rw-r--r--constrMatching.ml16484logplain
-rw-r--r--constrMatching.mli4071logplain
-rw-r--r--detyping.ml26891logplain
-rw-r--r--detyping.mli3077logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml45703logplain
-rw-r--r--evarconv.mli2789logplain
-rw-r--r--evarsolve.ml62324logplain
-rw-r--r--evarsolve.mli2918logplain
-rw-r--r--evarutil.ml30275logplain
-rw-r--r--evarutil.mli9096logplain
-rw-r--r--evd.ml54413logplain
-rw-r--r--evd.mli20066logplain
-rw-r--r--find_subterm.ml5601logplain
-rw-r--r--find_subterm.mli2843logplain
-rw-r--r--glob_ops.ml14087logplain
-rw-r--r--glob_ops.mli1769logplain
-rw-r--r--indrec.ml20739logplain
-rw-r--r--indrec.mli2346logplain
-rw-r--r--inductiveops.ml21144logplain
-rw-r--r--inductiveops.mli7591logplain
-rw-r--r--locusops.ml2773logplain
-rw-r--r--locusops.mli1304logplain
-rw-r--r--miscops.ml1244logplain
-rw-r--r--miscops.mli786logplain
-rw-r--r--namegen.ml13886logplain
-rw-r--r--namegen.mli4215logplain
-rw-r--r--nativenorm.ml13652logplain
-rw-r--r--nativenorm.mli752logplain
-rw-r--r--patternops.ml15583logplain
-rw-r--r--patternops.mli1977logplain
-rw-r--r--pretype_errors.ml6329logplain
-rw-r--r--pretype_errors.mli5097logplain
-rw-r--r--pretyping.ml35724logplain
-rw-r--r--pretyping.mli5106logplain
-rw-r--r--pretyping.mllib335logplain
-rw-r--r--program.ml2703logplain
-rw-r--r--program.mli1532logplain
-rw-r--r--recordops.ml11953logplain
-rw-r--r--recordops.mli2728logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml57779logplain
-rw-r--r--reductionops.mli11435logplain
-rw-r--r--retyping.ml9390logplain
-rw-r--r--retyping.mli1865logplain
-rw-r--r--tacred.ml43973logplain
-rw-r--r--tacred.mli3899logplain
-rw-r--r--termops.ml33605logplain
-rw-r--r--termops.mli9814logplain
-rw-r--r--typeclasses.ml18595logplain
-rw-r--r--typeclasses.mli5466logplain
-rw-r--r--typeclasses_errors.ml1248logplain
-rw-r--r--typeclasses_errors.mli1131logplain
-rw-r--r--typing.ml10548logplain
-rw-r--r--typing.mli1601logplain
-rw-r--r--unification.ml62677logplain
-rw-r--r--unification.mli4087logplain
-rw-r--r--vnorm.ml10839logplain
-rw-r--r--vnorm.mli629logplain