aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3611logplain
-rw-r--r--arguments_renaming.mli1003logplain
-rw-r--r--cases.ml100455logplain
-rw-r--r--cases.mli4268logplain
-rw-r--r--cbv.ml15126logplain
-rw-r--r--cbv.mli2150logplain
-rw-r--r--classops.ml17121logplain
-rw-r--r--classops.mli3781logplain
-rw-r--r--coercion.ml18134logplain
-rw-r--r--coercion.mli2941logplain
-rw-r--r--constr_matching.ml18388logplain
-rw-r--r--constr_matching.mli4134logplain
-rw-r--r--detyping.ml34783logplain
-rw-r--r--detyping.mli3502logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml50044logplain
-rw-r--r--evarconv.mli3010logplain
-rw-r--r--evardefine.ml7871logplain
-rw-r--r--evardefine.mli1803logplain
-rw-r--r--evarsolve.ml66033logplain
-rw-r--r--evarsolve.mli3031logplain
-rw-r--r--find_subterm.ml6594logplain
-rw-r--r--find_subterm.mli2923logplain
-rw-r--r--glob_ops.ml18109logplain
-rw-r--r--glob_ops.mli2698logplain
-rw-r--r--indrec.ml21647logplain
-rw-r--r--indrec.mli2364logplain
-rw-r--r--inductiveops.ml21533logplain
-rw-r--r--inductiveops.mli8133logplain
-rw-r--r--locusops.ml4029logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--miscops.ml2270logplain
-rw-r--r--miscops.mli1093logplain
-rw-r--r--nativenorm.ml14536logplain
-rw-r--r--nativenorm.mli848logplain
-rw-r--r--patternops.ml16105logplain
-rw-r--r--patternops.mli1978logplain
-rw-r--r--pretype_errors.ml6420logplain
-rw-r--r--pretype_errors.mli5179logplain
-rw-r--r--pretyping.ml42543logplain
-rw-r--r--pretyping.mli6309logplain
-rw-r--r--pretyping.mllib318logplain
-rw-r--r--program.ml2703logplain
-rw-r--r--program.mli1532logplain
-rw-r--r--recordops.ml12030logplain
-rw-r--r--recordops.mli2889logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml59558logplain
-rw-r--r--reductionops.mli12081logplain
-rw-r--r--retyping.ml9771logplain
-rw-r--r--retyping.mli1950logplain
-rw-r--r--tacred.ml46750logplain
-rw-r--r--tacred.mli3892logplain
-rw-r--r--typeclasses.ml18404logplain
-rw-r--r--typeclasses.mli5612logplain
-rw-r--r--typeclasses_errors.ml1228logplain
-rw-r--r--typeclasses_errors.mli1113logplain
-rw-r--r--typing.ml11312logplain
-rw-r--r--typing.mli1774logplain
-rw-r--r--unification.ml76482logplain
-rw-r--r--unification.mli4595logplain
-rw-r--r--vnorm.ml12785logplain
-rw-r--r--vnorm.mli628logplain