summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml62268logplain
-rw-r--r--cases.mli2026logplain
-rw-r--r--cbv.ml13455logplain
-rw-r--r--cbv.mli2049logplain
-rw-r--r--classops.ml11686logplain
-rw-r--r--classops.mli3202logplain
-rw-r--r--clenv.ml16149logplain
-rw-r--r--clenv.mli5252logplain
-rw-r--r--coercion.ml10447logplain
-rw-r--r--coercion.mli2667logplain
-rw-r--r--detyping.ml24012logplain
-rw-r--r--detyping.mli2310logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml19879logplain
-rw-r--r--evarconv.mli1406logplain
-rw-r--r--evarutil.ml29991logplain
-rw-r--r--evarutil.mli6163logplain
-rw-r--r--evd.ml17455logplain
-rw-r--r--evd.mli6203logplain
-rw-r--r--indrec.ml21677logplain
-rw-r--r--indrec.mli2275logplain
-rw-r--r--inductiveops.ml15066logplain
-rw-r--r--inductiveops.mli4915logplain
-rw-r--r--matching.ml10284logplain
-rw-r--r--matching.mli2046logplain
-rw-r--r--pattern.ml11134logplain
-rw-r--r--pattern.mli2734logplain
-rw-r--r--pretype_errors.ml6317logplain
-rw-r--r--pretype_errors.mli3669logplain
-rw-r--r--pretyping.ml25234logplain
-rw-r--r--pretyping.mli3635logplain
-rw-r--r--rawterm.ml12394logplain
-rw-r--r--rawterm.mli5535logplain
-rw-r--r--recordops.ml8332logplain
-rwxr-xr-xrecordops.mli1820logplain
-rw-r--r--reductionops.ml29070logplain
-rw-r--r--reductionops.mli8528logplain
-rw-r--r--retyping.ml6091logplain
-rw-r--r--retyping.mli1547logplain
-rw-r--r--tacred.ml30427logplain
-rw-r--r--tacred.mli2823logplain
-rw-r--r--termops.ml34604logplain
-rw-r--r--termops.mli8599logplain
-rw-r--r--typing.ml6119logplain
-rw-r--r--typing.mli1373logplain
-rw-r--r--unification.ml17766logplain
-rw-r--r--unification.mli1343logplain
-rw-r--r--vnorm.ml8941logplain
-rw-r--r--vnorm.mli662logplain