summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml68054logplain
-rw-r--r--cases.mli1901logplain
-rw-r--r--cbv.ml13097logplain
-rw-r--r--cbv.mli2042logplain
-rwxr-xr-xclassops.ml11756logplain
-rw-r--r--classops.mli3798logplain
-rw-r--r--coercion.ml7606logplain
-rw-r--r--coercion.mli1891logplain
-rw-r--r--detyping.ml18799logplain
-rw-r--r--detyping.mli1561logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml14285logplain
-rw-r--r--evarconv.mli1020logplain
-rw-r--r--evarutil.ml19180logplain
-rw-r--r--evarutil.mli3319logplain
-rw-r--r--evd.ml2115logplain
-rw-r--r--evd.mli1813logplain
-rw-r--r--indrec.ml19928logplain
-rw-r--r--indrec.mli2003logplain
-rw-r--r--inductiveops.ml12294logplain
-rw-r--r--inductiveops.mli4161logplain
-rw-r--r--instantiate.ml2024logplain
-rw-r--r--instantiate.mli1015logplain
-rw-r--r--matching.ml9153logplain
-rw-r--r--matching.mli1972logplain
-rw-r--r--pattern.ml10397logplain
-rw-r--r--pattern.mli2919logplain
-rw-r--r--pretype_errors.ml5435logplain
-rw-r--r--pretype_errors.mli3090logplain
-rw-r--r--pretyping.ml41091logplain
-rw-r--r--pretyping.mli2978logplain
-rw-r--r--rawterm.ml12935logplain
-rw-r--r--rawterm.mli4504logplain
-rwxr-xr-xrecordops.ml5532logplain
-rwxr-xr-xrecordops.mli1869logplain
-rw-r--r--reductionops.ml23995logplain
-rw-r--r--reductionops.mli7569logplain
-rw-r--r--retyping.ml5158logplain
-rw-r--r--retyping.mli1467logplain
-rw-r--r--tacred.ml32379logplain
-rw-r--r--tacred.mli2985logplain
-rw-r--r--termops.ml31762logplain
-rw-r--r--termops.mli7635logplain
-rw-r--r--typing.ml5310logplain
-rw-r--r--typing.mli976logplain