aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3569logplain
-rw-r--r--arguments_renaming.mli993logplain
-rw-r--r--cases.ml100240logplain
-rw-r--r--cases.mli4296logplain
-rw-r--r--cbv.ml15130logplain
-rw-r--r--cbv.mli2151logplain
-rw-r--r--classops.ml17109logplain
-rw-r--r--classops.mli3781logplain
-rw-r--r--coercion.ml18170logplain
-rw-r--r--coercion.mli2941logplain
-rw-r--r--constr_matching.ml19765logplain
-rw-r--r--constr_matching.mli4134logplain
-rw-r--r--detyping.ml34903logplain
-rw-r--r--detyping.mli3502logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml52391logplain
-rw-r--r--evarconv.mli3179logplain
-rw-r--r--evardefine.ml7821logplain
-rw-r--r--evardefine.mli1803logplain
-rw-r--r--evarsolve.ml67228logplain
-rw-r--r--evarsolve.mli3309logplain
-rw-r--r--find_subterm.ml6541logplain
-rw-r--r--find_subterm.mli2923logplain
-rw-r--r--glob_ops.ml21427logplain
-rw-r--r--glob_ops.mli3191logplain
-rw-r--r--indrec.ml21574logplain
-rw-r--r--indrec.mli2537logplain
-rw-r--r--inductiveops.ml22673logplain
-rw-r--r--inductiveops.mli8702logplain
-rw-r--r--locusops.ml4032logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--miscops.ml2270logplain
-rw-r--r--miscops.mli1093logplain
-rw-r--r--nativenorm.ml14511logplain
-rw-r--r--nativenorm.mli848logplain
-rw-r--r--patternops.ml16393logplain
-rw-r--r--patternops.mli1978logplain
-rw-r--r--pretype_errors.ml6526logplain
-rw-r--r--pretype_errors.mli5209logplain
-rw-r--r--pretyping.ml46735logplain
-rw-r--r--pretyping.mli6366logplain
-rw-r--r--pretyping.mllib318logplain
-rw-r--r--program.ml3935logplain
-rw-r--r--program.mli1663logplain
-rw-r--r--recordops.ml12434logplain
-rw-r--r--recordops.mli2889logplain
-rw-r--r--redops.ml1711logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml59466logplain
-rw-r--r--reductionops.mli11875logplain
-rw-r--r--retyping.ml9732logplain
-rw-r--r--retyping.mli2006logplain
-rw-r--r--tacred.ml46726logplain
-rw-r--r--tacred.mli3893logplain
-rw-r--r--typeclasses.ml18251logplain
-rw-r--r--typeclasses.mli5736logplain
-rw-r--r--typeclasses_errors.ml1228logplain
-rw-r--r--typeclasses_errors.mli1113logplain
-rw-r--r--typing.ml11654logplain
-rw-r--r--typing.mli1994logplain
-rw-r--r--unification.ml76122logplain
-rw-r--r--unification.mli4595logplain
-rw-r--r--vnorm.ml12844logplain
-rw-r--r--vnorm.mli628logplain