aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml67572logplain
-rw-r--r--cases.mli2460logplain
-rw-r--r--cbv.ml14356logplain
-rw-r--r--cbv.mli2097logplain
-rw-r--r--classops.ml12592logplain
-rw-r--r--classops.mli3403logplain
-rw-r--r--clenv.ml17153logplain
-rw-r--r--clenv.mli5534logplain
-rw-r--r--coercion.ml9774logplain
-rw-r--r--coercion.mli2923logplain
-rw-r--r--detyping.ml24737logplain
-rw-r--r--detyping.mli2299logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml20606logplain
-rw-r--r--evarconv.mli1574logplain
-rw-r--r--evarutil.ml52179logplain
-rw-r--r--evarutil.mli7799logplain
-rw-r--r--evd.ml26788logplain
-rw-r--r--evd.mli10184logplain
-rw-r--r--indrec.ml23143logplain
-rw-r--r--indrec.mli2215logplain
-rw-r--r--inductiveops.ml16693logplain
-rw-r--r--inductiveops.mli5054logplain
-rw-r--r--matching.ml11309logplain
-rw-r--r--matching.mli3610logplain
-rw-r--r--pattern.ml11336logplain
-rw-r--r--pattern.mli2686logplain
-rw-r--r--pretype_errors.ml6547logplain
-rw-r--r--pretype_errors.mli3891logplain
-rw-r--r--pretyping.ml26309logplain
-rw-r--r--pretyping.mli3749logplain
-rw-r--r--pretyping.mllib249logplain
-rw-r--r--rawterm.ml12777logplain
-rw-r--r--rawterm.mli5957logplain
-rw-r--r--recordops.ml11080logplain
-rwxr-xr-xrecordops.mli2702logplain
-rw-r--r--reductionops.ml32298logplain
-rw-r--r--reductionops.mli8899logplain
-rw-r--r--retyping.ml7046logplain
-rw-r--r--retyping.mli1523logplain
-rw-r--r--tacred.ml33832logplain
-rw-r--r--tacred.mli3287logplain
-rw-r--r--term_dnet.ml12639logplain
-rw-r--r--term_dnet.mli3458logplain
-rw-r--r--termops.ml40590logplain
-rw-r--r--termops.mli11888logplain
-rw-r--r--typeclasses.ml11717logplain
-rw-r--r--typeclasses.mli3552logplain
-rw-r--r--typeclasses_errors.ml2026logplain
-rw-r--r--typeclasses_errors.mli1518logplain
-rw-r--r--typing.ml5862logplain
-rw-r--r--typing.mli1325logplain
-rw-r--r--unification.ml36081logplain
-rw-r--r--unification.mli2037logplain
-rw-r--r--vnorm.ml10428logplain
-rw-r--r--vnorm.mli662logplain