aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3787logplain
-rw-r--r--arguments_renaming.mli995logplain
-rw-r--r--cases.ml92491logplain
-rw-r--r--cases.mli3884logplain
-rw-r--r--cbv.ml14108logplain
-rw-r--r--cbv.mli2071logplain
-rw-r--r--classops.ml13557logplain
-rw-r--r--classops.mli3419logplain
-rw-r--r--coercion.ml16087logplain
-rw-r--r--coercion.mli2728logplain
-rw-r--r--detyping.ml24980logplain
-rw-r--r--detyping.mli2863logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml32119logplain
-rw-r--r--evarconv.mli1951logplain
-rw-r--r--evarutil.ml79059logplain
-rw-r--r--evarutil.mli8899logplain
-rw-r--r--evd.ml30012logplain
-rw-r--r--evd.mli11427logplain
-rw-r--r--glob_term.ml14400logplain
-rw-r--r--glob_term.mli5822logplain
-rw-r--r--indrec.ml19846logplain
-rw-r--r--indrec.mli2379logplain
-rw-r--r--inductiveops.ml17284logplain
-rw-r--r--inductiveops.mli6043logplain
-rw-r--r--matching.ml12679logplain
-rw-r--r--matching.mli3947logplain
-rw-r--r--namegen.ml11664logplain
-rw-r--r--namegen.mli3658logplain
-rw-r--r--pattern.ml13787logplain
-rw-r--r--pattern.mli4762logplain
-rw-r--r--pretype_errors.ml6606logplain
-rw-r--r--pretype_errors.mli4485logplain
-rw-r--r--pretyping.ml27256logplain
-rw-r--r--pretyping.mli4231logplain
-rw-r--r--pretyping.mllib280logplain
-rw-r--r--program.ml2918logplain
-rw-r--r--recordops.ml12866logplain
-rw-r--r--recordops.mli3094logplain
-rw-r--r--reductionops.ml32448logplain
-rw-r--r--reductionops.mli9026logplain
-rw-r--r--retyping.ml7282logplain
-rw-r--r--retyping.mli1694logplain
-rw-r--r--tacred.ml38206logplain
-rw-r--r--tacred.mli3724logplain
-rw-r--r--term_dnet.ml13148logplain
-rw-r--r--term_dnet.mli3448logplain
-rw-r--r--termops.ml38572logplain
-rw-r--r--termops.mli11467logplain
-rw-r--r--typeclasses.ml16137logplain
-rw-r--r--typeclasses.mli4572logplain
-rw-r--r--typeclasses_errors.ml2027logplain
-rw-r--r--typeclasses_errors.mli1502logplain
-rw-r--r--typing.ml10096logplain
-rw-r--r--typing.mli1553logplain
-rw-r--r--unification.ml47374logplain
-rw-r--r--unification.mli2893logplain
-rw-r--r--vnorm.ml10376logplain
-rw-r--r--vnorm.mli655logplain