summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml62343logplain
-rw-r--r--cases.mli1669logplain
-rw-r--r--cbv.ml13455logplain
-rw-r--r--cbv.mli2049logplain
-rw-r--r--classops.ml11627logplain
-rw-r--r--classops.mli3202logplain
-rw-r--r--clenv.ml15069logplain
-rw-r--r--clenv.mli4278logplain
-rw-r--r--coercion.ml10373logplain
-rw-r--r--coercion.mli2667logplain
-rw-r--r--detyping.ml23741logplain
-rw-r--r--detyping.mli2251logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml17497logplain
-rw-r--r--evarconv.mli1327logplain
-rw-r--r--evarutil.ml24118logplain
-rw-r--r--evarutil.mli5640logplain
-rw-r--r--evd.ml17296logplain
-rw-r--r--evd.mli5980logplain
-rw-r--r--indrec.ml21679logplain
-rw-r--r--indrec.mli2275logplain
-rw-r--r--inductiveops.ml14948logplain
-rw-r--r--inductiveops.mli4856logplain
-rw-r--r--matching.ml10233logplain
-rw-r--r--matching.mli2046logplain
-rw-r--r--pattern.ml11135logplain
-rw-r--r--pattern.mli2734logplain
-rw-r--r--pretype_errors.ml6132logplain
-rw-r--r--pretype_errors.mli3508logplain
-rw-r--r--pretyping.ml26008logplain
-rw-r--r--pretyping.mli3642logplain
-rw-r--r--rawterm.ml10048logplain
-rw-r--r--rawterm.mli5028logplain
-rw-r--r--recordops.ml8273logplain
-rwxr-xr-xrecordops.mli1826logplain
-rw-r--r--reductionops.ml28820logplain
-rw-r--r--reductionops.mli8459logplain
-rw-r--r--retyping.ml5847logplain
-rw-r--r--retyping.mli1541logplain
-rw-r--r--tacred.ml30181logplain
-rw-r--r--tacred.mli2823logplain
-rw-r--r--termops.ml34261logplain
-rw-r--r--termops.mli8295logplain
-rw-r--r--typing.ml5505logplain
-rw-r--r--typing.mli1373logplain
-rw-r--r--unification.ml16603logplain
-rw-r--r--unification.mli1343logplain