aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml67146logplain
-rw-r--r--cases.mli1883logplain
-rw-r--r--cbv.ml13037logplain
-rw-r--r--cbv.mli1979logplain
-rwxr-xr-xclassops.ml11653logplain
-rw-r--r--classops.mli3732logplain
-rw-r--r--coercion.ml7541logplain
-rw-r--r--coercion.mli1830logplain
-rw-r--r--detyping.ml17381logplain
-rw-r--r--detyping.mli1592logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml14144logplain
-rw-r--r--evarconv.mli953logplain
-rw-r--r--evarutil.ml19718logplain
-rw-r--r--evarutil.mli3244logplain
-rw-r--r--evd.ml2056logplain
-rw-r--r--evd.mli1753logplain
-rw-r--r--indrec.ml19602logplain
-rw-r--r--indrec.mli1940logplain
-rw-r--r--inductiveops.ml12028logplain
-rw-r--r--inductiveops.mli4028logplain
-rw-r--r--instantiate.ml1957logplain
-rw-r--r--instantiate.mli946logplain
-rw-r--r--matching.ml8960logplain
-rw-r--r--matching.mli1896logplain
-rw-r--r--pattern.ml10402logplain
-rw-r--r--pattern.mli2831logplain
-rw-r--r--pretype_errors.ml5324logplain
-rw-r--r--pretype_errors.mli2975logplain
-rw-r--r--pretyping.ml39128logplain
-rw-r--r--pretyping.mli2667logplain
-rw-r--r--rawterm.ml10608logplain
-rw-r--r--rawterm.mli4259logplain
-rwxr-xr-xrecordops.ml5440logplain
-rwxr-xr-xrecordops.mli1802logplain
-rw-r--r--reductionops.ml24610logplain
-rw-r--r--reductionops.mli7877logplain
-rw-r--r--retyping.ml4878logplain
-rw-r--r--retyping.mli1401logplain
-rw-r--r--tacred.ml30700logplain
-rw-r--r--tacred.mli2568logplain
-rw-r--r--termops.ml28339logplain
-rw-r--r--termops.mli7511logplain
-rw-r--r--typing.ml5263logplain
-rw-r--r--typing.mli912logplain