aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml71374logplain
-rw-r--r--cases.mli2461logplain
-rw-r--r--cbv.ml13413logplain
-rw-r--r--cbv.mli2006logplain
-rw-r--r--classops.ml12912logplain
-rw-r--r--classops.mli3412logplain
-rw-r--r--clenv.ml17393logplain
-rw-r--r--clenv.mli5536logplain
-rw-r--r--coercion.ml9722logplain
-rw-r--r--coercion.mli2944logplain
-rw-r--r--detyping.ml25124logplain
-rw-r--r--detyping.mli2302logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20173logplain
-rw-r--r--evarconv.mli1356logplain
-rw-r--r--evarutil.ml47824logplain
-rw-r--r--evarutil.mli7458logplain
-rw-r--r--evd.ml22950logplain
-rw-r--r--evd.mli9241logplain
-rw-r--r--indrec.ml21701logplain
-rw-r--r--indrec.mli2252logplain
-rw-r--r--inductiveops.ml16409logplain
-rw-r--r--inductiveops.mli5032logplain
-rw-r--r--matching.ml11030logplain
-rw-r--r--matching.mli3403logplain
-rw-r--r--pattern.ml11129logplain
-rw-r--r--pattern.mli2687logplain
-rw-r--r--pretype_errors.ml6551logplain
-rw-r--r--pretype_errors.mli3898logplain
-rw-r--r--pretyping.ml28104logplain
-rw-r--r--pretyping.mli3769logplain
-rw-r--r--rawterm.ml13194logplain
-rw-r--r--rawterm.mli6021logplain
-rw-r--r--recordops.ml9453logplain
-rwxr-xr-xrecordops.mli2078logplain
-rw-r--r--reductionops.ml32240logplain
-rw-r--r--reductionops.mli9001logplain
-rw-r--r--retyping.ml6803logplain
-rw-r--r--retyping.mli1599logplain
-rw-r--r--tacred.ml29613logplain
-rw-r--r--tacred.mli3065logplain
-rw-r--r--termops.ml37044logplain
-rw-r--r--termops.mli10519logplain
-rw-r--r--typeclasses.ml11813logplain
-rw-r--r--typeclasses.mli3278logplain
-rw-r--r--typeclasses_errors.ml1925logplain
-rw-r--r--typeclasses_errors.mli1480logplain
-rw-r--r--typing.ml6058logplain
-rw-r--r--typing.mli1327logplain
-rw-r--r--unification.ml28933logplain
-rw-r--r--unification.mli1857logplain
-rw-r--r--vnorm.ml10496logplain
-rw-r--r--vnorm.mli662logplain