aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3611logplain
-rw-r--r--arguments_renaming.mli1003logplain
-rw-r--r--cases.ml99651logplain
-rw-r--r--cases.mli4209logplain
-rw-r--r--cbv.ml15126logplain
-rw-r--r--cbv.mli2150logplain
-rw-r--r--classops.ml17112logplain
-rw-r--r--classops.mli3709logplain
-rw-r--r--coercion.ml17930logplain
-rw-r--r--coercion.mli2941logplain
-rw-r--r--constr_matching.ml18279logplain
-rw-r--r--constr_matching.mli4134logplain
-rw-r--r--detyping.ml34064logplain
-rw-r--r--detyping.mli3513logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml51632logplain
-rw-r--r--evarconv.mli3010logplain
-rw-r--r--evarsolve.ml65930logplain
-rw-r--r--evarsolve.mli3172logplain
-rw-r--r--evarutil.ml32209logplain
-rw-r--r--evarutil.mli10497logplain
-rw-r--r--evd.ml64918logplain
-rw-r--r--evd.mli23971logplain
-rw-r--r--find_subterm.ml6355logplain
-rw-r--r--find_subterm.mli2896logplain
-rw-r--r--glob_ops.ml18102logplain
-rw-r--r--glob_ops.mli2698logplain
-rw-r--r--indrec.ml21605logplain
-rw-r--r--indrec.mli2346logplain
-rw-r--r--inductiveops.ml21905logplain
-rw-r--r--inductiveops.mli8052logplain
-rw-r--r--locusops.ml4029logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--miscops.ml2270logplain
-rw-r--r--miscops.mli1093logplain
-rw-r--r--namegen.ml14059logplain
-rw-r--r--namegen.mli4215logplain
-rw-r--r--nativenorm.ml14446logplain
-rw-r--r--nativenorm.mli866logplain
-rw-r--r--patternops.ml16041logplain
-rw-r--r--patternops.mli1991logplain
-rw-r--r--pretype_errors.ml6525logplain
-rw-r--r--pretype_errors.mli5209logplain
-rw-r--r--pretyping.ml41337logplain
-rw-r--r--pretyping.mli5969logplain
-rw-r--r--pretyping.mllib336logplain
-rw-r--r--program.ml2703logplain
-rw-r--r--program.mli1532logplain
-rw-r--r--recordops.ml12041logplain
-rw-r--r--recordops.mli2889logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml60330logplain
-rw-r--r--reductionops.mli12301logplain
-rw-r--r--retyping.ml9675logplain
-rw-r--r--retyping.mli1961logplain
-rw-r--r--tacred.ml45665logplain
-rw-r--r--tacred.mli3922logplain
-rw-r--r--termops.ml35200logplain
-rw-r--r--termops.mli10158logplain
-rw-r--r--typeclasses.ml18428logplain
-rw-r--r--typeclasses.mli5619logplain
-rw-r--r--typeclasses_errors.ml1239logplain
-rw-r--r--typeclasses_errors.mli1122logplain
-rw-r--r--typing.ml11254logplain
-rw-r--r--typing.mli1768logplain
-rw-r--r--unification.ml75115logplain
-rw-r--r--unification.mli4587logplain
-rw-r--r--vnorm.ml12814logplain
-rw-r--r--vnorm.mli637logplain