aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3537logplain
-rw-r--r--arguments_renaming.mli1116logplain
-rw-r--r--cases.ml106404logplain
-rw-r--r--cases.mli4665logplain
-rw-r--r--cbv.ml17864logplain
-rw-r--r--cbv.mli2325logplain
-rw-r--r--classops.ml17639logplain
-rw-r--r--classops.mli3905logplain
-rw-r--r--coercion.ml19117logplain
-rw-r--r--coercion.mli3129logplain
-rw-r--r--constr_matching.ml22097logplain
-rw-r--r--constr_matching.mli3326logplain
-rw-r--r--constrexpr.ml6120logplain
-rw-r--r--detyping.ml41156logplain
-rw-r--r--detyping.mli4172logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml58145logplain
-rw-r--r--evarconv.mli3717logplain
-rw-r--r--evardefine.ml7803logplain
-rw-r--r--evardefine.mli1966logplain
-rw-r--r--evarsolve.ml70726logplain
-rw-r--r--evarsolve.mli3499logplain
-rw-r--r--extend.ml5010logplain
-rw-r--r--find_subterm.ml6844logplain
-rw-r--r--find_subterm.mli3062logplain
-rw-r--r--geninterp.ml2731logplain
-rw-r--r--geninterp.mli2480logplain
-rw-r--r--genredexpr.ml2049logplain
-rw-r--r--glob_ops.ml21980logplain
-rw-r--r--glob_ops.mli4260logplain
-rw-r--r--glob_term.ml5896logplain
-rw-r--r--indrec.ml23128logplain
-rw-r--r--indrec.mli2665logplain
-rw-r--r--inductiveops.ml24380logplain
-rw-r--r--inductiveops.mli9294logplain
-rw-r--r--inferCumulativity.ml8256logplain
-rw-r--r--inferCumulativity.mli780logplain
-rw-r--r--locus.ml3096logplain
-rw-r--r--locusops.ml4207logplain
-rw-r--r--locusops.mli1775logplain
-rw-r--r--ltac_pretype.ml2556logplain
-rw-r--r--miscops.ml2858logplain
-rw-r--r--miscops.mli1424logplain
-rw-r--r--nativenorm.ml17890logplain
-rw-r--r--nativenorm.mli1171logplain
-rw-r--r--pattern.ml2002logplain
-rw-r--r--patternops.ml21754logplain
-rw-r--r--patternops.mli2202logplain
-rw-r--r--pretype_errors.ml6819logplain
-rw-r--r--pretype_errors.mli5647logplain
-rw-r--r--pretyping.ml49730logplain
-rw-r--r--pretyping.mli5324logplain
-rw-r--r--pretyping.mllib433logplain
-rw-r--r--program.ml3610logplain
-rw-r--r--program.mli1748logplain
-rw-r--r--recordops.ml13894logplain
-rw-r--r--recordops.mli2975logplain
-rw-r--r--redops.ml1885logplain
-rw-r--r--redops.mli784logplain
-rw-r--r--reductionops.ml62305logplain
-rw-r--r--reductionops.mli12566logplain
-rw-r--r--retyping.ml10576logplain
-rw-r--r--retyping.mli2413logplain
-rw-r--r--tacred.ml48305logplain
-rw-r--r--tacred.mli4029logplain
-rw-r--r--typeclasses.ml19431logplain
-rw-r--r--typeclasses.mli6311logplain
-rw-r--r--typeclasses_errors.ml1359logplain
-rw-r--r--typeclasses_errors.mli1236logplain
-rw-r--r--typing.ml16675logplain
-rw-r--r--typing.mli2935logplain
-rw-r--r--unification.ml77890logplain
-rw-r--r--unification.mli4466logplain
-rw-r--r--univdecls.ml2296logplain
-rw-r--r--univdecls.mli1119logplain
-rw-r--r--vernacexpr.ml19811logplain
-rw-r--r--vnorm.ml14926logplain
-rw-r--r--vnorm.mli797logplain