summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3611logplain
-rw-r--r--arguments_renaming.mli1003logplain
-rw-r--r--cases.ml98027logplain
-rw-r--r--cases.mli4209logplain
-rw-r--r--cbv.ml15116logplain
-rw-r--r--cbv.mli2150logplain
-rw-r--r--classops.ml17127logplain
-rw-r--r--classops.mli3687logplain
-rw-r--r--coercion.ml17704logplain
-rw-r--r--coercion.mli2941logplain
-rw-r--r--constr_matching.ml18693logplain
-rw-r--r--constr_matching.mli4071logplain
-rw-r--r--detyping.ml33312logplain
-rw-r--r--detyping.mli3513logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml49565logplain
-rw-r--r--evarconv.mli3010logplain
-rw-r--r--evarsolve.ml62410logplain
-rw-r--r--evarsolve.mli3025logplain
-rw-r--r--evarutil.ml31257logplain
-rw-r--r--evarutil.mli9686logplain
-rw-r--r--evd.ml59376logplain
-rw-r--r--evd.mli23235logplain
-rw-r--r--find_subterm.ml6422logplain
-rw-r--r--find_subterm.mli2907logplain
-rw-r--r--glob_ops.ml15925logplain
-rw-r--r--glob_ops.mli2494logplain
-rw-r--r--indrec.ml21315logplain
-rw-r--r--indrec.mli2346logplain
-rw-r--r--inductiveops.ml21424logplain
-rw-r--r--inductiveops.mli7591logplain
-rw-r--r--locusops.ml4029logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--miscops.ml2244logplain
-rw-r--r--miscops.mli1093logplain
-rw-r--r--namegen.ml14019logplain
-rw-r--r--namegen.mli4215logplain
-rw-r--r--nativenorm.ml14115logplain
-rw-r--r--nativenorm.mli752logplain
-rw-r--r--patternops.ml16012logplain
-rw-r--r--patternops.mli2007logplain
-rw-r--r--pretype_errors.ml6420logplain
-rw-r--r--pretype_errors.mli5179logplain
-rw-r--r--pretyping.ml38643logplain
-rw-r--r--pretyping.mli5389logplain
-rw-r--r--pretyping.mllib336logplain
-rw-r--r--program.ml2703logplain
-rw-r--r--program.mli1532logplain
-rw-r--r--recordops.ml12009logplain
-rw-r--r--recordops.mli2889logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml58879logplain
-rw-r--r--reductionops.mli11510logplain
-rw-r--r--retyping.ml9737logplain
-rw-r--r--retyping.mli1961logplain
-rw-r--r--tacred.ml45814logplain
-rw-r--r--tacred.mli3922logplain
-rw-r--r--termops.ml35018logplain
-rw-r--r--termops.mli10038logplain
-rw-r--r--typeclasses.ml18560logplain
-rw-r--r--typeclasses.mli5663logplain
-rw-r--r--typeclasses_errors.ml1248logplain
-rw-r--r--typeclasses_errors.mli1131logplain
-rw-r--r--typing.ml10509logplain
-rw-r--r--typing.mli1600logplain
-rw-r--r--unification.ml72769logplain
-rw-r--r--unification.mli4546logplain
-rw-r--r--vnorm.ml11089logplain
-rw-r--r--vnorm.mli629logplain