summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3537logplain
-rw-r--r--arguments_renaming.mli1116logplain
-rw-r--r--cases.ml106932logplain
-rw-r--r--cases.mli4665logplain
-rw-r--r--cbv.ml17790logplain
-rw-r--r--cbv.mli2294logplain
-rw-r--r--classops.ml17603logplain
-rw-r--r--classops.mli3901logplain
-rw-r--r--coercion.ml19734logplain
-rw-r--r--coercion.mli3129logplain
-rw-r--r--constr_matching.ml22296logplain
-rw-r--r--constr_matching.mli3326logplain
-rw-r--r--detyping.ml41302logplain
-rw-r--r--detyping.mli4166logplain
-rw-r--r--evarconv.ml58333logplain
-rw-r--r--evarconv.mli3717logplain
-rw-r--r--evardefine.ml7812logplain
-rw-r--r--evardefine.mli1966logplain
-rw-r--r--evarsolve.ml70672logplain
-rw-r--r--evarsolve.mli3499logplain
-rw-r--r--find_subterm.ml6844logplain
-rw-r--r--find_subterm.mli3062logplain
-rw-r--r--geninterp.ml2731logplain
-rw-r--r--geninterp.mli2489logplain
-rw-r--r--glob_ops.ml22641logplain
-rw-r--r--glob_ops.mli4471logplain
-rw-r--r--glob_term.ml6007logplain
-rw-r--r--heads.ml6539logplain
-rw-r--r--heads.mli1247logplain
-rw-r--r--indrec.ml23189logplain
-rw-r--r--indrec.mli2689logplain
-rw-r--r--inductiveops.ml29174logplain
-rw-r--r--inductiveops.mli9985logplain
-rw-r--r--inferCumulativity.ml8278logplain
-rw-r--r--inferCumulativity.mli780logplain
-rw-r--r--locus.ml3137logplain
-rw-r--r--locusops.ml4187logplain
-rw-r--r--locusops.mli1775logplain
-rw-r--r--ltac_pretype.ml2556logplain
-rw-r--r--nativenorm.ml18586logplain
-rw-r--r--nativenorm.mli1171logplain
-rw-r--r--pattern.ml2029logplain
-rw-r--r--patternops.ml21703logplain
-rw-r--r--patternops.mli2187logplain
-rw-r--r--pretype_errors.ml6832logplain
-rw-r--r--pretype_errors.mli5647logplain
-rw-r--r--pretyping.ml49580logplain
-rw-r--r--pretyping.mli5324logplain
-rw-r--r--pretyping.mllib382logplain
-rw-r--r--program.ml3610logplain
-rw-r--r--program.mli1748logplain
-rw-r--r--recordops.ml15150logplain
-rw-r--r--recordops.mli3226logplain
-rw-r--r--reductionops.ml62282logplain
-rw-r--r--reductionops.mli12719logplain
-rw-r--r--retyping.ml10283logplain
-rw-r--r--retyping.mli2413logplain
-rw-r--r--tacred.ml48002logplain
-rw-r--r--tacred.mli4029logplain
-rw-r--r--typeclasses.ml19457logplain
-rw-r--r--typeclasses.mli6297logplain
-rw-r--r--typeclasses_errors.ml1137logplain
-rw-r--r--typeclasses_errors.mli1014logplain
-rw-r--r--typing.ml16529logplain
-rw-r--r--typing.mli2935logplain
-rw-r--r--unification.ml79118logplain
-rw-r--r--unification.mli4490logplain
-rw-r--r--vnorm.ml15221logplain
-rw-r--r--vnorm.mli797logplain