aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml67694logplain
-rw-r--r--cases.mli2461logplain
-rw-r--r--cbv.ml14375logplain
-rw-r--r--cbv.mli2097logplain
-rw-r--r--classops.ml12565logplain
-rw-r--r--classops.mli3412logplain
-rw-r--r--clenv.ml17184logplain
-rw-r--r--clenv.mli5536logplain
-rw-r--r--coercion.ml9818logplain
-rw-r--r--coercion.mli2944logplain
-rw-r--r--detyping.ml24820logplain
-rw-r--r--detyping.mli2302logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20631logplain
-rw-r--r--evarconv.mli1577logplain
-rw-r--r--evarutil.ml52246logplain
-rw-r--r--evarutil.mli7605logplain
-rw-r--r--evd.ml27003logplain
-rw-r--r--evd.mli10197logplain
-rw-r--r--indrec.ml23140logplain
-rw-r--r--indrec.mli2217logplain
-rw-r--r--inductiveops.ml16583logplain
-rw-r--r--inductiveops.mli5017logplain
-rw-r--r--matching.ml11320logplain
-rw-r--r--matching.mli3613logplain
-rw-r--r--pattern.ml11280logplain
-rw-r--r--pattern.mli2687logplain
-rw-r--r--pretype_errors.ml6551logplain
-rw-r--r--pretype_errors.mli3898logplain
-rw-r--r--pretyping.ml26468logplain
-rw-r--r--pretyping.mli3828logplain
-rw-r--r--pretyping.mllib249logplain
-rw-r--r--rawterm.ml12816logplain
-rw-r--r--rawterm.mli5962logplain
-rw-r--r--recordops.ml11248logplain
-rwxr-xr-xrecordops.mli2709logplain
-rw-r--r--reductionops.ml32518logplain
-rw-r--r--reductionops.mli8904logplain
-rw-r--r--retyping.ml7049logplain
-rw-r--r--retyping.mli1525logplain
-rw-r--r--tacred.ml33944logplain
-rw-r--r--tacred.mli3375logplain
-rw-r--r--term_dnet.ml12679logplain
-rw-r--r--term_dnet.mli3472logplain
-rw-r--r--termops.ml40527logplain
-rw-r--r--termops.mli11902logplain
-rw-r--r--typeclasses.ml10635logplain
-rw-r--r--typeclasses.mli3256logplain
-rw-r--r--typeclasses_errors.ml2031logplain
-rw-r--r--typeclasses_errors.mli1519logplain
-rw-r--r--typing.ml5902logplain
-rw-r--r--typing.mli1327logplain
-rw-r--r--unification.ml35692logplain
-rw-r--r--unification.mli2039logplain
-rw-r--r--vnorm.ml10496logplain
-rw-r--r--vnorm.mli662logplain