aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml64119logplain
-rw-r--r--cases.mli1657logplain
-rw-r--r--cbv.ml13037logplain
-rw-r--r--cbv.mli1988logplain
-rw-r--r--classops.ml11581logplain
-rw-r--r--classops.mli3152logplain
-rw-r--r--clenv.ml14999logplain
-rw-r--r--clenv.mli4231logplain
-rw-r--r--coercion.ml6687logplain
-rw-r--r--coercion.mli1873logplain
-rw-r--r--detyping.ml23702logplain
-rw-r--r--detyping.mli1799logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml17450logplain
-rw-r--r--evarconv.mli1279logplain
-rw-r--r--evarutil.ml21854logplain
-rw-r--r--evarutil.mli4432logplain
-rw-r--r--evd.ml17127logplain
-rw-r--r--evd.mli5943logplain
-rw-r--r--indrec.ml21621logplain
-rw-r--r--indrec.mli2227logplain
-rw-r--r--inductiveops.ml13686logplain
-rw-r--r--inductiveops.mli4541logplain
-rw-r--r--matching.ml9425logplain
-rw-r--r--matching.mli1996logplain
-rw-r--r--pattern.ml9353logplain
-rw-r--r--pattern.mli2534logplain
-rw-r--r--pretype_errors.ml5973logplain
-rw-r--r--pretype_errors.mli3381logplain
-rw-r--r--pretyping.ml21340logplain
-rw-r--r--pretyping.mli2852logplain
-rw-r--r--rawterm.ml9639logplain
-rw-r--r--rawterm.mli4674logplain
-rw-r--r--recordops.ml8053logplain
-rwxr-xr-xrecordops.mli1866logplain
-rw-r--r--reductionops.ml26141logplain
-rw-r--r--reductionops.mli7765logplain
-rw-r--r--retyping.ml5114logplain
-rw-r--r--retyping.mli1379logplain
-rw-r--r--tacred.ml30136logplain
-rw-r--r--tacred.mli2776logplain
-rw-r--r--termops.ml34216logplain
-rw-r--r--termops.mli8249logplain
-rw-r--r--typing.ml5454logplain
-rw-r--r--typing.mli1327logplain
-rw-r--r--unification.ml16550logplain
-rw-r--r--unification.mli1290logplain