aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3628logplain
-rw-r--r--arguments_renaming.mli993logplain
-rw-r--r--cases.ml103730logplain
-rw-r--r--cases.mli4236logplain
-rw-r--r--cbv.ml15180logplain
-rw-r--r--cbv.mli2159logplain
-rw-r--r--classops.ml17447logplain
-rw-r--r--classops.mli3796logplain
-rw-r--r--coercion.ml19291logplain
-rw-r--r--coercion.mli2954logplain
-rw-r--r--constr_matching.ml19153logplain
-rw-r--r--constr_matching.mli4170logplain
-rw-r--r--detyping.ml35288logplain
-rw-r--r--detyping.mli3502logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml54438logplain
-rw-r--r--evarconv.mli2999logplain
-rw-r--r--evardefine.ml8342logplain
-rw-r--r--evardefine.mli1816logplain
-rw-r--r--evarsolve.ml69616logplain
-rw-r--r--evarsolve.mli3215logplain
-rw-r--r--find_subterm.ml6776logplain
-rw-r--r--find_subterm.mli3029logplain
-rw-r--r--glob_ops.ml21427logplain
-rw-r--r--glob_ops.mli3191logplain
-rw-r--r--indrec.ml22019logplain
-rw-r--r--indrec.mli2537logplain
-rw-r--r--inductiveops.ml23625logplain
-rw-r--r--inductiveops.mli8904logplain
-rw-r--r--locusops.ml4032logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--miscops.ml2639logplain
-rw-r--r--miscops.mli1254logplain
-rw-r--r--nativenorm.ml15030logplain
-rw-r--r--nativenorm.mli854logplain
-rw-r--r--patternops.ml16730logplain
-rw-r--r--patternops.mli2002logplain
-rw-r--r--pretype_errors.ml6973logplain
-rw-r--r--pretype_errors.mli6111logplain
-rw-r--r--pretyping.ml48229logplain
-rw-r--r--pretyping.mli6351logplain
-rw-r--r--pretyping.mllib318logplain
-rw-r--r--program.ml4022logplain
-rw-r--r--program.mli1666logplain
-rw-r--r--recordops.ml12630logplain
-rw-r--r--recordops.mli2869logplain
-rw-r--r--redops.ml1711logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml62745logplain
-rw-r--r--reductionops.mli12355logplain
-rw-r--r--retyping.ml10875logplain
-rw-r--r--retyping.mli2110logplain
-rw-r--r--tacred.ml49019logplain
-rw-r--r--tacred.mli3997logplain
-rw-r--r--typeclasses.ml18809logplain
-rw-r--r--typeclasses.mli5720logplain
-rw-r--r--typeclasses_errors.ml1241logplain
-rw-r--r--typeclasses_errors.mli1126logplain
-rw-r--r--typing.ml15167logplain
-rw-r--r--typing.mli2464logplain
-rw-r--r--unification.ml79875logplain
-rw-r--r--unification.mli4374logplain
-rw-r--r--vnorm.ml13654logplain
-rw-r--r--vnorm.mli649logplain