aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml61107logplain
-rw-r--r--cases.mli1980logplain
-rw-r--r--cbv.ml13413logplain
-rw-r--r--cbv.mli2006logplain
-rw-r--r--classops.ml11637logplain
-rw-r--r--classops.mli3152logplain
-rw-r--r--clenv.ml15980logplain
-rw-r--r--clenv.mli5354logplain
-rw-r--r--coercion.ml10398logplain
-rw-r--r--coercion.mli2618logplain
-rw-r--r--detyping.ml24148logplain
-rw-r--r--detyping.mli2261logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml19830logplain
-rw-r--r--evarconv.mli1356logplain
-rw-r--r--evarutil.ml29950logplain
-rw-r--r--evarutil.mli6116logplain
-rw-r--r--evd.ml19509logplain
-rw-r--r--evd.mli7404logplain
-rw-r--r--indrec.ml21733logplain
-rw-r--r--indrec.mli2252logplain
-rw-r--r--inductiveops.ml14841logplain
-rw-r--r--inductiveops.mli4859logplain
-rw-r--r--matching.ml10235logplain
-rw-r--r--matching.mli1996logplain
-rw-r--r--pattern.ml11107logplain
-rw-r--r--pattern.mli2687logplain
-rw-r--r--pretype_errors.ml6247logplain
-rw-r--r--pretype_errors.mli3588logplain
-rw-r--r--pretyping.ml25385logplain
-rw-r--r--pretyping.mli3584logplain
-rw-r--r--rawterm.ml12347logplain
-rw-r--r--rawterm.mli5487logplain
-rw-r--r--recordops.ml8282logplain
-rwxr-xr-xrecordops.mli1769logplain
-rw-r--r--reductionops.ml30631logplain
-rw-r--r--reductionops.mli8609logplain
-rw-r--r--retyping.ml6042logplain
-rw-r--r--retyping.mli1497logplain
-rw-r--r--tacred.ml31236logplain
-rw-r--r--tacred.mli3043logplain
-rw-r--r--termops.ml35380logplain
-rw-r--r--termops.mli9537logplain
-rw-r--r--typing.ml6072logplain
-rw-r--r--typing.mli1327logplain
-rw-r--r--unification.ml24196logplain
-rw-r--r--unification.mli1346logplain
-rw-r--r--vnorm.ml10842logplain
-rw-r--r--vnorm.mli662logplain