aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml67686logplain
-rw-r--r--cases.mli2439logplain
-rw-r--r--cbv.ml14356logplain
-rw-r--r--cbv.mli2073logplain
-rw-r--r--classops.ml12592logplain
-rw-r--r--classops.mli3421logplain
-rw-r--r--coercion.ml9933logplain
-rw-r--r--coercion.mli2897logplain
-rw-r--r--detyping.ml24931logplain
-rw-r--r--detyping.mli2274logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20632logplain
-rw-r--r--evarconv.mli1535logplain
-rw-r--r--evarutil.ml55942logplain
-rw-r--r--evarutil.mli7985logplain
-rw-r--r--evd.ml27962logplain
-rw-r--r--evd.mli10744logplain
-rw-r--r--indrec.ml19574logplain
-rw-r--r--indrec.mli2381logplain
-rw-r--r--inductiveops.ml16707logplain
-rw-r--r--inductiveops.mli5146logplain
-rw-r--r--matching.ml11313logplain
-rw-r--r--matching.mli3602logplain
-rw-r--r--namegen.ml10973logplain
-rw-r--r--namegen.mli3394logplain
-rw-r--r--pattern.ml12274logplain
-rw-r--r--pattern.mli2700logplain
-rw-r--r--pretype_errors.ml6785logplain
-rw-r--r--pretype_errors.mli3897logplain
-rw-r--r--pretyping.ml26771logplain
-rw-r--r--pretyping.mli3828logplain
-rw-r--r--pretyping.mllib251logplain
-rw-r--r--rawterm.ml12786logplain
-rw-r--r--rawterm.mli5966logplain
-rw-r--r--recordops.ml11066logplain
-rwxr-xr-xrecordops.mli2917logplain
-rw-r--r--reductionops.ml32465logplain
-rw-r--r--reductionops.mli8967logplain
-rw-r--r--retyping.ml7046logplain
-rw-r--r--retyping.mli1502logplain
-rw-r--r--tacred.ml33957logplain
-rw-r--r--tacred.mli3331logplain
-rw-r--r--term_dnet.ml13154logplain
-rw-r--r--term_dnet.mli3462logplain
-rw-r--r--termops.ml32840logplain
-rw-r--r--termops.mli9844logplain
-rw-r--r--typeclasses.ml11861logplain
-rw-r--r--typeclasses.mli3424logplain
-rw-r--r--typeclasses_errors.ml2025logplain
-rw-r--r--typeclasses_errors.mli1494logplain
-rw-r--r--typing.ml7273logplain
-rw-r--r--typing.mli1184logplain
-rw-r--r--unification.ml36202logplain
-rw-r--r--unification.mli2002logplain
-rw-r--r--vnorm.ml10428logplain
-rw-r--r--vnorm.mli643logplain