aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml65801logplain
-rw-r--r--cases.mli2436logplain
-rw-r--r--cbv.ml14344logplain
-rw-r--r--cbv.mli2059logplain
-rw-r--r--classops.ml12580logplain
-rw-r--r--classops.mli3414logplain
-rw-r--r--coercion.ml10337logplain
-rw-r--r--coercion.mli2883logplain
-rw-r--r--detyping.ml24919logplain
-rw-r--r--detyping.mli2260logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20880logplain
-rw-r--r--evarconv.mli1528logplain
-rw-r--r--evarutil.ml58901logplain
-rw-r--r--evarutil.mli7985logplain
-rw-r--r--evd.ml28302logplain
-rw-r--r--evd.mli10737logplain
-rw-r--r--indrec.ml19570logplain
-rw-r--r--indrec.mli2367logplain
-rw-r--r--inductiveops.ml16699logplain
-rw-r--r--inductiveops.mli5132logplain
-rw-r--r--matching.ml12650logplain
-rw-r--r--matching.mli3935logplain
-rw-r--r--namegen.ml10961logplain
-rw-r--r--namegen.mli3319logplain
-rw-r--r--pattern.ml13135logplain
-rw-r--r--pattern.mli4360logplain
-rw-r--r--pretype_errors.ml7244logplain
-rw-r--r--pretype_errors.mli4149logplain
-rw-r--r--pretyping.ml27502logplain
-rw-r--r--pretyping.mli4082logplain
-rw-r--r--pretyping.mllib251logplain
-rw-r--r--rawterm.ml12774logplain
-rw-r--r--rawterm.mli5548logplain
-rw-r--r--recordops.ml11281logplain
-rwxr-xr-xrecordops.mli2985logplain
-rw-r--r--reductionops.ml32445logplain
-rw-r--r--reductionops.mli8933logplain
-rw-r--r--retyping.ml7034logplain
-rw-r--r--retyping.mli1488logplain
-rw-r--r--tacred.ml33945logplain
-rw-r--r--tacred.mli3317logplain
-rw-r--r--term_dnet.ml13141logplain
-rw-r--r--term_dnet.mli3436logplain
-rw-r--r--termops.ml33625logplain
-rw-r--r--termops.mli10002logplain
-rw-r--r--typeclasses.ml11757logplain
-rw-r--r--typeclasses.mli3410logplain
-rw-r--r--typeclasses_errors.ml2019logplain
-rw-r--r--typeclasses_errors.mli1480logplain
-rw-r--r--typing.ml7261logplain
-rw-r--r--typing.mli1170logplain
-rw-r--r--unification.ml36300logplain
-rw-r--r--unification.mli1988logplain
-rw-r--r--vnorm.ml10414logplain
-rw-r--r--vnorm.mli643logplain