summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml71418logplain
-rw-r--r--cases.mli2509logplain
-rw-r--r--cbv.ml13455logplain
-rw-r--r--cbv.mli2049logplain
-rw-r--r--classops.ml11719logplain
-rw-r--r--classops.mli3244logplain
-rw-r--r--clenv.ml17420logplain
-rw-r--r--clenv.mli5584logplain
-rw-r--r--coercion.ml9733logplain
-rw-r--r--coercion.mli2806logplain
-rw-r--r--detyping.ml24941logplain
-rw-r--r--detyping.mli2352logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml19903logplain
-rw-r--r--evarconv.mli1406logplain
-rw-r--r--evarutil.ml47300logplain
-rw-r--r--evarutil.mli7043logplain
-rw-r--r--evd.ml22845logplain
-rw-r--r--evd.mli9006logplain
-rw-r--r--indrec.ml21777logplain
-rw-r--r--indrec.mli2300logplain
-rw-r--r--inductiveops.ml14309logplain
-rw-r--r--inductiveops.mli4913logplain
-rw-r--r--matching.ml10312logplain
-rw-r--r--matching.mli2046logplain
-rw-r--r--pattern.ml11173logplain
-rw-r--r--pattern.mli2734logplain
-rw-r--r--pretype_errors.ml6607logplain
-rw-r--r--pretype_errors.mli3955logplain
-rw-r--r--pretyping.ml26608logplain
-rw-r--r--pretyping.mli3820logplain
-rw-r--r--rawterm.ml12821logplain
-rw-r--r--rawterm.mli5974logplain
-rw-r--r--recordops.ml8939logplain
-rwxr-xr-xrecordops.mli2027logplain
-rw-r--r--reductionops.ml32280logplain
-rw-r--r--reductionops.mli9030logplain
-rw-r--r--retyping.ml6319logplain
-rw-r--r--retyping.mli1547logplain
-rw-r--r--tacred.ml29624logplain
-rw-r--r--tacred.mli3114logplain
-rw-r--r--termops.ml36733logplain
-rw-r--r--termops.mli10314logplain
-rw-r--r--typeclasses.ml13861logplain
-rw-r--r--typeclasses.mli3943logplain
-rw-r--r--typeclasses_errors.ml1986logplain
-rw-r--r--typeclasses_errors.mli1544logplain
-rw-r--r--typing.ml6106logplain
-rw-r--r--typing.mli1373logplain
-rw-r--r--unification.ml27787logplain
-rw-r--r--unification.mli1911logplain
-rw-r--r--vnorm.ml10304logplain
-rw-r--r--vnorm.mli662logplain