aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3394logplain
-rw-r--r--arguments_renaming.mli995logplain
-rw-r--r--cases.ml106109logplain
-rw-r--r--cases.mli4515logplain
-rw-r--r--cbv.ml17612logplain
-rw-r--r--cbv.mli2173logplain
-rw-r--r--classops.ml17500logplain
-rw-r--r--classops.mli3772logplain
-rw-r--r--coercion.ml18690logplain
-rw-r--r--coercion.mli2979logplain
-rw-r--r--constr_matching.ml19255logplain
-rw-r--r--constr_matching.mli3169logplain
-rw-r--r--detyping.ml40021logplain
-rw-r--r--detyping.mli3710logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml59859logplain
-rw-r--r--evarconv.mli3284logplain
-rw-r--r--evardefine.ml7598logplain
-rw-r--r--evardefine.mli1816logplain
-rw-r--r--evarsolve.ml71462logplain
-rw-r--r--evarsolve.mli3345logplain
-rw-r--r--find_subterm.ml6694logplain
-rw-r--r--find_subterm.mli2912logplain
-rw-r--r--geninterp.ml2581logplain
-rw-r--r--geninterp.mli2330logplain
-rw-r--r--glob_ops.ml20610logplain
-rw-r--r--glob_ops.mli3765logplain
-rw-r--r--indrec.ml22968logplain
-rw-r--r--indrec.mli2532logplain
-rw-r--r--inductiveops.ml27717logplain
-rw-r--r--inductiveops.mli9558logplain
-rw-r--r--locusops.ml4057logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--ltac_pretype.ml2556logplain
-rw-r--r--miscops.ml2682logplain
-rw-r--r--miscops.mli1254logplain
-rw-r--r--nativenorm.ml17241logplain
-rw-r--r--nativenorm.mli1021logplain
-rw-r--r--patternops.ml18714logplain
-rw-r--r--patternops.mli2070logplain
-rw-r--r--pretype_errors.ml6669logplain
-rw-r--r--pretype_errors.mli5497logplain
-rw-r--r--pretyping.ml49304logplain
-rw-r--r--pretyping.mli4888logplain
-rw-r--r--pretyping.mllib351logplain
-rw-r--r--program.ml3424logplain
-rw-r--r--program.mli1728logplain
-rw-r--r--recordops.ml13254logplain
-rw-r--r--recordops.mli2882logplain
-rw-r--r--redops.ml1735logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml64925logplain
-rw-r--r--reductionops.mli12690logplain
-rw-r--r--retyping.ml10474logplain
-rw-r--r--retyping.mli2261logplain
-rw-r--r--tacred.ml48187logplain
-rw-r--r--tacred.mli3959logplain
-rw-r--r--typeclasses.ml19186logplain
-rw-r--r--typeclasses.mli5933logplain
-rw-r--r--typeclasses_errors.ml1231logplain
-rw-r--r--typeclasses_errors.mli1116logplain
-rw-r--r--typing.ml14567logplain
-rw-r--r--typing.mli2326logplain
-rw-r--r--unification.ml79296logplain
-rw-r--r--unification.mli4316logplain
-rw-r--r--univdecls.ml2129logplain
-rw-r--r--univdecls.mli975logplain
-rw-r--r--vnorm.ml13686logplain
-rw-r--r--vnorm.mli647logplain