aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml66388logplain
-rw-r--r--cases.mli2454logplain
-rw-r--r--cbv.ml14093logplain
-rw-r--r--cbv.mli2071logplain
-rw-r--r--classops.ml13515logplain
-rw-r--r--classops.mli3419logplain
-rw-r--r--coercion.ml10504logplain
-rw-r--r--coercion.mli2897logplain
-rw-r--r--detyping.ml24891logplain
-rw-r--r--detyping.mli2864logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml28469logplain
-rw-r--r--evarconv.mli1911logplain
-rw-r--r--evarutil.ml65263logplain
-rw-r--r--evarutil.mli8198logplain
-rw-r--r--evd.ml29626logplain
-rw-r--r--evd.mli11220logplain
-rw-r--r--glob_term.ml14358logplain
-rw-r--r--glob_term.mli5816logplain
-rw-r--r--indrec.ml19827logplain
-rw-r--r--indrec.mli2379logplain
-rw-r--r--inductiveops.ml16394logplain
-rw-r--r--inductiveops.mli5397logplain
-rw-r--r--matching.ml12475logplain
-rw-r--r--matching.mli3947logplain
-rw-r--r--namegen.ml11303logplain
-rw-r--r--namegen.mli3629logplain
-rw-r--r--pattern.ml12951logplain
-rw-r--r--pattern.mli4398logplain
-rw-r--r--pretype_errors.ml6588logplain
-rw-r--r--pretype_errors.mli4473logplain
-rw-r--r--pretyping.ml28651logplain
-rw-r--r--pretyping.mli4402logplain
-rw-r--r--pretyping.mllib253logplain
-rw-r--r--recordops.ml12787logplain
-rw-r--r--recordops.mli3079logplain
-rw-r--r--reductionops.ml32367logplain
-rw-r--r--reductionops.mli8979logplain
-rw-r--r--retyping.ml7270logplain
-rw-r--r--retyping.mli1694logplain
-rw-r--r--tacred.ml33645logplain
-rw-r--r--tacred.mli3331logplain
-rw-r--r--term_dnet.ml13141logplain
-rw-r--r--term_dnet.mli3448logplain
-rw-r--r--termops.ml37647logplain
-rw-r--r--termops.mli11277logplain
-rw-r--r--typeclasses.ml13281logplain
-rw-r--r--typeclasses.mli3996logplain
-rw-r--r--typeclasses_errors.ml2019logplain
-rw-r--r--typeclasses_errors.mli1492logplain
-rw-r--r--typing.ml10039logplain
-rw-r--r--typing.mli1553logplain
-rw-r--r--unification.ml45426logplain
-rw-r--r--unification.mli2858logplain
-rw-r--r--vnorm.ml10438logplain
-rw-r--r--vnorm.mli655logplain