aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml66425logplain
-rw-r--r--cases.mli1828logplain
-rw-r--r--cbv.ml13037logplain
-rw-r--r--cbv.mli1979logplain
-rwxr-xr-xclassops.ml11691logplain
-rw-r--r--classops.mli3732logplain
-rw-r--r--coercion.ml7541logplain
-rw-r--r--coercion.mli1830logplain
-rw-r--r--detyping.ml17739logplain
-rw-r--r--detyping.mli1462logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml14144logplain
-rw-r--r--evarconv.mli953logplain
-rw-r--r--evarutil.ml19743logplain
-rw-r--r--evarutil.mli3251logplain
-rw-r--r--evd.ml2056logplain
-rw-r--r--evd.mli1753logplain
-rw-r--r--indrec.ml19602logplain
-rw-r--r--indrec.mli1940logplain
-rw-r--r--inductiveops.ml12209logplain
-rw-r--r--inductiveops.mli4087logplain
-rw-r--r--instantiate.ml1957logplain
-rw-r--r--instantiate.mli946logplain
-rw-r--r--matching.ml9089logplain
-rw-r--r--matching.mli1905logplain
-rw-r--r--pattern.ml10384logplain
-rw-r--r--pattern.mli2854logplain
-rw-r--r--pretype_errors.ml5324logplain
-rw-r--r--pretype_errors.mli2975logplain
-rw-r--r--pretyping.ml39861logplain
-rw-r--r--pretyping.mli2911logplain
-rw-r--r--rawterm.ml12030logplain
-rw-r--r--rawterm.mli4338logplain
-rwxr-xr-xrecordops.ml5478logplain
-rwxr-xr-xrecordops.mli1802logplain
-rw-r--r--reductionops.ml24610logplain
-rw-r--r--reductionops.mli7877logplain
-rw-r--r--retyping.ml5093logplain
-rw-r--r--retyping.mli1401logplain
-rw-r--r--tacred.ml32039logplain
-rw-r--r--tacred.mli2919logplain
-rw-r--r--termops.ml29805logplain
-rw-r--r--termops.mli7524logplain
-rw-r--r--typing.ml5263logplain
-rw-r--r--typing.mli912logplain