aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3611logplain
-rw-r--r--arguments_renaming.mli1003logplain
-rw-r--r--cases.ml96629logplain
-rw-r--r--cases.mli4209logplain
-rw-r--r--cbv.ml14480logplain
-rw-r--r--cbv.mli2150logplain
-rw-r--r--classops.ml17041logplain
-rw-r--r--classops.mli3682logplain
-rw-r--r--coercion.ml17733logplain
-rw-r--r--coercion.mli2935logplain
-rw-r--r--constrMatching.ml19700logplain
-rw-r--r--constrMatching.mli4071logplain
-rw-r--r--detyping.ml28369logplain
-rw-r--r--detyping.mli3234logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml46686logplain
-rw-r--r--evarconv.mli2789logplain
-rw-r--r--evarsolve.ml62107logplain
-rw-r--r--evarsolve.mli2918logplain
-rw-r--r--evarutil.ml30419logplain
-rw-r--r--evarutil.mli9217logplain
-rw-r--r--evd.ml58950logplain
-rw-r--r--evd.mli21094logplain
-rw-r--r--find_subterm.ml5655logplain
-rw-r--r--find_subterm.mli2843logplain
-rw-r--r--glob_ops.ml13914logplain
-rw-r--r--glob_ops.mli1769logplain
-rw-r--r--indrec.ml21254logplain
-rw-r--r--indrec.mli2346logplain
-rw-r--r--inductiveops.ml21190logplain
-rw-r--r--inductiveops.mli7591logplain
-rw-r--r--locusops.ml2773logplain
-rw-r--r--locusops.mli1304logplain
-rw-r--r--miscops.ml1211logplain
-rw-r--r--miscops.mli786logplain
-rw-r--r--namegen.ml13918logplain
-rw-r--r--namegen.mli4215logplain
-rw-r--r--nativenorm.ml13652logplain
-rw-r--r--nativenorm.mli752logplain
-rw-r--r--patternops.ml15527logplain
-rw-r--r--patternops.mli1977logplain
-rw-r--r--pretype_errors.ml6329logplain
-rw-r--r--pretype_errors.mli5097logplain
-rw-r--r--pretyping.ml37497logplain
-rw-r--r--pretyping.mli5180logplain
-rw-r--r--pretyping.mllib335logplain
-rw-r--r--program.ml2703logplain
-rw-r--r--program.mli1532logplain
-rw-r--r--recordops.ml11953logplain
-rw-r--r--recordops.mli2728logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml57560logplain
-rw-r--r--reductionops.mli11442logplain
-rw-r--r--retyping.ml9386logplain
-rw-r--r--retyping.mli1865logplain
-rw-r--r--tacred.ml44335logplain
-rw-r--r--tacred.mli3910logplain
-rw-r--r--termops.ml33605logplain
-rw-r--r--termops.mli9814logplain
-rw-r--r--typeclasses.ml18544logplain
-rw-r--r--typeclasses.mli5663logplain
-rw-r--r--typeclasses_errors.ml1248logplain
-rw-r--r--typeclasses_errors.mli1131logplain
-rw-r--r--typing.ml10510logplain
-rw-r--r--typing.mli1600logplain
-rw-r--r--unification.ml64644logplain
-rw-r--r--unification.mli4316logplain
-rw-r--r--vnorm.ml10839logplain
-rw-r--r--vnorm.mli629logplain