aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml65799logplain
-rw-r--r--cases.mli2448logplain
-rw-r--r--cbv.ml14344logplain
-rw-r--r--cbv.mli2071logplain
-rw-r--r--classops.ml13184logplain
-rw-r--r--classops.mli3426logplain
-rw-r--r--coercion.ml10337logplain
-rw-r--r--coercion.mli2895logplain
-rw-r--r--detyping.ml24964logplain
-rw-r--r--detyping.mli2272logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20877logplain
-rw-r--r--evarconv.mli1540logplain
-rw-r--r--evarutil.ml58675logplain
-rw-r--r--evarutil.mli7756logplain
-rw-r--r--evd.ml28486logplain
-rw-r--r--evd.mli10804logplain
-rw-r--r--indrec.ml19570logplain
-rw-r--r--indrec.mli2379logplain
-rw-r--r--inductiveops.ml16699logplain
-rw-r--r--inductiveops.mli5144logplain
-rw-r--r--matching.ml12650logplain
-rw-r--r--matching.mli3947logplain
-rw-r--r--namegen.ml10961logplain
-rw-r--r--namegen.mli3331logplain
-rw-r--r--pattern.ml13137logplain
-rw-r--r--pattern.mli4388logplain
-rw-r--r--pretype_errors.ml7244logplain
-rw-r--r--pretype_errors.mli4161logplain
-rw-r--r--pretyping.ml27696logplain
-rw-r--r--pretyping.mli4094logplain
-rw-r--r--pretyping.mllib251logplain
-rw-r--r--rawterm.ml14292logplain
-rw-r--r--rawterm.mli5361logplain
-rw-r--r--recordops.ml12544logplain
-rw-r--r--recordops.mli3045logplain
-rw-r--r--reductionops.ml32445logplain
-rw-r--r--reductionops.mli8945logplain
-rw-r--r--retyping.ml7034logplain
-rw-r--r--retyping.mli1500logplain
-rw-r--r--tacred.ml33945logplain
-rw-r--r--tacred.mli3329logplain
-rw-r--r--term_dnet.ml13141logplain
-rw-r--r--term_dnet.mli3448logplain
-rw-r--r--termops.ml33822logplain
-rw-r--r--termops.mli10063logplain
-rw-r--r--typeclasses.ml11757logplain
-rw-r--r--typeclasses.mli3422logplain
-rw-r--r--typeclasses_errors.ml2019logplain
-rw-r--r--typeclasses_errors.mli1492logplain
-rw-r--r--typing.ml7261logplain
-rw-r--r--typing.mli1182logplain
-rw-r--r--unification.ml37043logplain
-rw-r--r--unification.mli2000logplain
-rw-r--r--vnorm.ml10438logplain
-rw-r--r--vnorm.mli655logplain