summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml71612logplain
-rw-r--r--cases.mli2509logplain
-rw-r--r--cbv.ml13634logplain
-rw-r--r--cbv.mli2066logplain
-rw-r--r--classops.ml12952logplain
-rw-r--r--classops.mli3463logplain
-rw-r--r--clenv.ml17502logplain
-rw-r--r--clenv.mli5584logplain
-rw-r--r--coercion.ml9772logplain
-rw-r--r--coercion.mli2994logplain
-rw-r--r--detyping.ml24943logplain
-rw-r--r--detyping.mli2352logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20537logplain
-rw-r--r--evarconv.mli1406logplain
-rw-r--r--evarutil.ml50854logplain
-rw-r--r--evarutil.mli7587logplain
-rw-r--r--evd.ml23121logplain
-rw-r--r--evd.mli9328logplain
-rw-r--r--indrec.ml21746logplain
-rw-r--r--indrec.mli2266logplain
-rw-r--r--inductiveops.ml16461logplain
-rw-r--r--inductiveops.mli5085logplain
-rw-r--r--matching.ml11370logplain
-rw-r--r--matching.mli3664logplain
-rw-r--r--pattern.ml11178logplain
-rw-r--r--pattern.mli2734logplain
-rw-r--r--pretype_errors.ml6607logplain
-rw-r--r--pretype_errors.mli3955logplain
-rw-r--r--pretyping.ml26671logplain
-rw-r--r--pretyping.mli3820logplain
-rw-r--r--rawterm.ml12845logplain
-rw-r--r--rawterm.mli5992logplain
-rw-r--r--recordops.ml9693logplain
-rwxr-xr-xrecordops.mli2376logplain
-rw-r--r--reductionops.ml31924logplain
-rw-r--r--reductionops.mli8829logplain
-rw-r--r--retyping.ml7166logplain
-rw-r--r--retyping.mli1642logplain
-rw-r--r--tacred.ml33064logplain
-rw-r--r--tacred.mli3114logplain
-rw-r--r--termops.ml37529logplain
-rw-r--r--termops.mli10678logplain
-rw-r--r--typeclasses.ml11865logplain
-rw-r--r--typeclasses.mli3331logplain
-rw-r--r--typeclasses_errors.ml1984logplain
-rw-r--r--typeclasses_errors.mli1540logplain
-rw-r--r--typing.ml6106logplain
-rw-r--r--typing.mli1373logplain
-rw-r--r--unification.ml30226logplain
-rw-r--r--unification.mli1911logplain
-rw-r--r--vnorm.ml10542logplain
-rw-r--r--vnorm.mli662logplain