aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3544logplain
-rw-r--r--arguments_renaming.mli1145logplain
-rw-r--r--cases.ml106182logplain
-rw-r--r--cases.mli4665logplain
-rw-r--r--cbv.ml17787logplain
-rw-r--r--cbv.mli2323logplain
-rw-r--r--classops.ml17650logplain
-rw-r--r--classops.mli3922logplain
-rw-r--r--coercion.ml18840logplain
-rw-r--r--coercion.mli3129logplain
-rw-r--r--constr_matching.ml19405logplain
-rw-r--r--constr_matching.mli3319logplain
-rw-r--r--detyping.ml40061logplain
-rw-r--r--detyping.mli3860logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml59550logplain
-rw-r--r--evarconv.mli3434logplain
-rw-r--r--evardefine.ml7756logplain
-rw-r--r--evardefine.mli1966logplain
-rw-r--r--evarsolve.ml71612logplain
-rw-r--r--evarsolve.mli3495logplain
-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--glob_ops.ml21921logplain
-rw-r--r--glob_ops.mli4260logplain
-rw-r--r--indrec.ml23118logplain
-rw-r--r--indrec.mli2682logplain
-rw-r--r--inductiveops.ml24380logplain
-rw-r--r--inductiveops.mli9290logplain
-rw-r--r--inferCumulativity.ml8154logplain
-rw-r--r--inferCumulativity.mli780logplain
-rw-r--r--locusops.ml4207logplain
-rw-r--r--locusops.mli1775logplain
-rw-r--r--ltac_pretype.ml2556logplain
-rw-r--r--miscops.ml2832logplain
-rw-r--r--miscops.mli1404logplain
-rw-r--r--nativenorm.ml17887logplain
-rw-r--r--nativenorm.mli1171logplain
-rw-r--r--patternops.ml18874logplain
-rw-r--r--patternops.mli2220logplain
-rw-r--r--pretype_errors.ml6819logplain
-rw-r--r--pretype_errors.mli5647logplain
-rw-r--r--pretyping.ml49663logplain
-rw-r--r--pretyping.mli5334logplain
-rw-r--r--pretyping.mllib369logplain
-rw-r--r--program.ml3574logplain
-rw-r--r--program.mli1878logplain
-rw-r--r--recordops.ml13893logplain
-rw-r--r--recordops.mli3032logplain
-rw-r--r--redops.ml1885logplain
-rw-r--r--redops.mli784logplain
-rw-r--r--reductionops.ml62498logplain
-rw-r--r--reductionops.mli12820logplain
-rw-r--r--retyping.ml10624logplain
-rw-r--r--retyping.mli2411logplain
-rw-r--r--tacred.ml48278logplain
-rw-r--r--tacred.mli4109logplain
-rw-r--r--typeclasses.ml19336logplain
-rw-r--r--typeclasses.mli6280logplain
-rw-r--r--typeclasses_errors.ml1381logplain
-rw-r--r--typeclasses_errors.mli1266logplain
-rw-r--r--typing.ml15841logplain
-rw-r--r--typing.mli2570logplain
-rw-r--r--unification.ml78472logplain
-rw-r--r--unification.mli4466logplain
-rw-r--r--univdecls.ml2281logplain
-rw-r--r--univdecls.mli1119logplain
-rw-r--r--vnorm.ml14834logplain
-rw-r--r--vnorm.mli797logplain