aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml63182logplain
-rw-r--r--cases.mli1741logplain
-rw-r--r--cbv.ml13037logplain
-rw-r--r--cbv.mli1979logplain
-rwxr-xr-xclassops.ml11749logplain
-rw-r--r--classops.mli3733logplain
-rw-r--r--coercion.ml7541logplain
-rw-r--r--coercion.mli1830logplain
-rw-r--r--detyping.ml14945logplain
-rw-r--r--detyping.mli1585logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml14144logplain
-rw-r--r--evarconv.mli953logplain
-rw-r--r--evarutil.ml19675logplain
-rw-r--r--evarutil.mli3232logplain
-rw-r--r--evd.ml1991logplain
-rw-r--r--evd.mli1704logplain
-rw-r--r--indrec.ml21502logplain
-rw-r--r--indrec.mli1912logplain
-rw-r--r--inductiveops.ml10851logplain
-rw-r--r--inductiveops.mli4028logplain
-rw-r--r--instantiate.ml1948logplain
-rw-r--r--instantiate.mli946logplain
-rw-r--r--matching.ml8960logplain
-rw-r--r--matching.mli1896logplain
-rw-r--r--pattern.ml10183logplain
-rw-r--r--pattern.mli2831logplain
-rw-r--r--pretype_errors.ml5300logplain
-rw-r--r--pretype_errors.mli2927logplain
-rw-r--r--pretyping.ml23344logplain
-rw-r--r--pretyping.mli2667logplain
-rw-r--r--rawterm.ml9236logplain
-rw-r--r--rawterm.mli3889logplain
-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.ml27348logplain
-rw-r--r--termops.mli7196logplain
-rw-r--r--typing.ml5263logplain
-rw-r--r--typing.mli912logplain