aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3508logplain
-rw-r--r--arguments_renaming.mli1000logplain
-rw-r--r--cases.ml92728logplain
-rw-r--r--cases.mli3877logplain
-rw-r--r--cbv.ml14069logplain
-rw-r--r--cbv.mli2073logplain
-rw-r--r--classops.ml15075logplain
-rw-r--r--classops.mli3600logplain
-rw-r--r--coercion.ml16187logplain
-rw-r--r--coercion.mli2735logplain
-rw-r--r--detyping.ml25745logplain
-rw-r--r--detyping.mli2950logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml37337logplain
-rw-r--r--evarconv.mli2737logplain
-rw-r--r--evarsolve.ml56535logplain
-rw-r--r--evarsolve.mli2574logplain
-rw-r--r--evarutil.ml27491logplain
-rw-r--r--evarutil.mli7914logplain
-rw-r--r--evd.ml28952logplain
-rw-r--r--evd.mli12832logplain
-rw-r--r--glob_ops.ml9937logplain
-rw-r--r--glob_ops.mli1799logplain
-rw-r--r--indrec.ml19951logplain
-rw-r--r--indrec.mli2367logplain
-rw-r--r--inductiveops.ml17635logplain
-rw-r--r--inductiveops.mli6046logplain
-rw-r--r--locusops.ml2773logplain
-rw-r--r--locusops.mli1319logplain
-rw-r--r--matching.ml14762logplain
-rw-r--r--matching.mli4048logplain
-rw-r--r--miscops.ml2075logplain
-rw-r--r--miscops.mli1003logplain
-rw-r--r--namegen.ml11919logplain
-rw-r--r--namegen.mli3537logplain
-rw-r--r--nativenorm.ml12347logplain
-rw-r--r--nativenorm.mli699logplain
-rw-r--r--patternops.ml15101logplain
-rw-r--r--patternops.mli2022logplain
-rw-r--r--pretype_errors.ml5491logplain
-rw-r--r--pretype_errors.mli4551logplain
-rw-r--r--pretyping.ml30058logplain
-rw-r--r--pretyping.mli4540logplain
-rw-r--r--pretyping.mllib326logplain
-rw-r--r--program.ml2580logplain
-rw-r--r--program.mli1229logplain
-rw-r--r--recordops.ml11102logplain
-rw-r--r--recordops.mli2716logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml38944logplain
-rw-r--r--reductionops.mli9921logplain
-rw-r--r--retyping.ml8711logplain
-rw-r--r--retyping.mli1903logplain
-rw-r--r--tacred.ml40283logplain
-rw-r--r--tacred.mli3739logplain
-rw-r--r--term_dnet.ml11016logplain
-rw-r--r--term_dnet.mli2637logplain
-rw-r--r--termops.ml38332logplain
-rw-r--r--termops.mli11471logplain
-rw-r--r--typeclasses.ml16574logplain
-rw-r--r--typeclasses.mli4982logplain
-rw-r--r--typeclasses_errors.ml1968logplain
-rw-r--r--typeclasses_errors.mli1587logplain
-rw-r--r--typing.ml10298logplain
-rw-r--r--typing.mli1546logplain
-rw-r--r--unification.ml48822logplain
-rw-r--r--unification.mli3033logplain
-rw-r--r--vnorm.ml10591logplain
-rw-r--r--vnorm.mli655logplain