aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3788logplain
-rw-r--r--arguments_renaming.mli996logplain
-rw-r--r--cases.ml92604logplain
-rw-r--r--cases.mli3890logplain
-rw-r--r--cbv.ml14108logplain
-rw-r--r--cbv.mli2071logplain
-rw-r--r--classops.ml13579logplain
-rw-r--r--classops.mli3420logplain
-rw-r--r--coercion.ml16120logplain
-rw-r--r--coercion.mli2732logplain
-rw-r--r--detyping.ml25235logplain
-rw-r--r--detyping.mli2975logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml32628logplain
-rw-r--r--evarconv.mli1962logplain
-rw-r--r--evarutil.ml79093logplain
-rw-r--r--evarutil.mli8909logplain
-rw-r--r--evd.ml29838logplain
-rw-r--r--evd.mli10784logplain
-rw-r--r--glob_ops.ml9499logplain
-rw-r--r--glob_ops.mli1733logplain
-rw-r--r--indrec.ml19864logplain
-rw-r--r--indrec.mli2379logplain
-rw-r--r--inductiveops.ml17284logplain
-rw-r--r--inductiveops.mli6043logplain
-rw-r--r--locusops.ml2698logplain
-rw-r--r--locusops.mli1276logplain
-rw-r--r--matching.ml12741logplain
-rw-r--r--matching.mli3947logplain
-rw-r--r--miscops.ml1862logplain
-rw-r--r--miscops.mli1003logplain
-rw-r--r--namegen.ml11679logplain
-rw-r--r--namegen.mli3658logplain
-rw-r--r--patternops.ml12814logplain
-rw-r--r--patternops.mli1980logplain
-rw-r--r--pretype_errors.ml6592logplain
-rw-r--r--pretype_errors.mli4487logplain
-rw-r--r--pretyping.ml27703logplain
-rw-r--r--pretyping.mli4245logplain
-rw-r--r--pretyping.mllib306logplain
-rw-r--r--program.ml2919logplain
-rw-r--r--program.mli1229logplain
-rw-r--r--recordops.ml12888logplain
-rw-r--r--recordops.mli3095logplain
-rw-r--r--redops.ml1437logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml33933logplain
-rw-r--r--reductionops.mli9232logplain
-rw-r--r--retyping.ml7282logplain
-rw-r--r--retyping.mli1694logplain
-rw-r--r--tacred.ml38374logplain
-rw-r--r--tacred.mli3739logplain
-rw-r--r--term_dnet.ml13149logplain
-rw-r--r--term_dnet.mli3448logplain
-rw-r--r--termops.ml38214logplain
-rw-r--r--termops.mli11153logplain
-rw-r--r--typeclasses.ml16371logplain
-rw-r--r--typeclasses.mli4756logplain
-rw-r--r--typeclasses_errors.ml2028logplain
-rw-r--r--typeclasses_errors.mli1504logplain
-rw-r--r--typing.ml10096logplain
-rw-r--r--typing.mli1553logplain
-rw-r--r--unification.ml47821logplain
-rw-r--r--unification.mli2893logplain
-rw-r--r--vnorm.ml10376logplain
-rw-r--r--vnorm.mli655logplain