aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3394logplain
-rw-r--r--arguments_renaming.mli995logplain
-rw-r--r--cases.ml106032logplain
-rw-r--r--cases.mli4515logplain
-rw-r--r--cbv.ml17637logplain
-rw-r--r--cbv.mli2173logplain
-rw-r--r--classops.ml17500logplain
-rw-r--r--classops.mli3772logplain
-rw-r--r--coercion.ml18690logplain
-rw-r--r--coercion.mli2979logplain
-rw-r--r--constr_matching.ml19255logplain
-rw-r--r--constr_matching.mli3169logplain
-rw-r--r--detyping.ml39911logplain
-rw-r--r--detyping.mli3710logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml59400logplain
-rw-r--r--evarconv.mli3284logplain
-rw-r--r--evardefine.ml7606logplain
-rw-r--r--evardefine.mli1816logplain
-rw-r--r--evarsolve.ml71462logplain
-rw-r--r--evarsolve.mli3345logplain
-rw-r--r--find_subterm.ml6694logplain
-rw-r--r--find_subterm.mli2912logplain
-rw-r--r--geninterp.ml2581logplain
-rw-r--r--geninterp.mli2330logplain
-rw-r--r--glob_ops.ml21771logplain
-rw-r--r--glob_ops.mli4110logplain
-rw-r--r--indrec.ml22968logplain
-rw-r--r--indrec.mli2532logplain
-rw-r--r--inductiveops.ml24180logplain
-rw-r--r--inductiveops.mli9116logplain
-rw-r--r--inferCumulativity.ml8004logplain
-rw-r--r--inferCumulativity.mli630logplain
-rw-r--r--locusops.ml4057logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--ltac_pretype.ml2556logplain
-rw-r--r--miscops.ml2682logplain
-rw-r--r--miscops.mli1254logplain
-rw-r--r--nativenorm.ml17737logplain
-rw-r--r--nativenorm.mli1021logplain
-rw-r--r--patternops.ml18724logplain
-rw-r--r--patternops.mli2070logplain
-rw-r--r--pretype_errors.ml6669logplain
-rw-r--r--pretype_errors.mli5497logplain
-rw-r--r--pretyping.ml49682logplain
-rw-r--r--pretyping.mli5197logplain
-rw-r--r--pretyping.mllib369logplain
-rw-r--r--program.ml3424logplain
-rw-r--r--program.mli1728logplain
-rw-r--r--recordops.ml13743logplain
-rw-r--r--recordops.mli2882logplain
-rw-r--r--redops.ml1735logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml62404logplain
-rw-r--r--reductionops.mli12672logplain
-rw-r--r--retyping.ml10474logplain
-rw-r--r--retyping.mli2261logplain
-rw-r--r--tacred.ml48128logplain
-rw-r--r--tacred.mli3959logplain
-rw-r--r--typeclasses.ml19186logplain
-rw-r--r--typeclasses.mli6130logplain
-rw-r--r--typeclasses_errors.ml1231logplain
-rw-r--r--typeclasses_errors.mli1116logplain
-rw-r--r--typing.ml15691logplain
-rw-r--r--typing.mli2420logplain
-rw-r--r--unification.ml79304logplain
-rw-r--r--unification.mli4316logplain
-rw-r--r--univdecls.ml2131logplain
-rw-r--r--univdecls.mli969logplain
-rw-r--r--vnorm.ml13830logplain
-rw-r--r--vnorm.mli647logplain