aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3633logplain
-rw-r--r--arguments_renaming.mli995logplain
-rw-r--r--cases.ml106164logplain
-rw-r--r--cases.mli4515logplain
-rw-r--r--cbv.ml17607logplain
-rw-r--r--cbv.mli2168logplain
-rw-r--r--classops.ml17313logplain
-rw-r--r--classops.mli3753logplain
-rw-r--r--coercion.ml18690logplain
-rw-r--r--coercion.mli2979logplain
-rw-r--r--constr_matching.ml21000logplain
-rw-r--r--constr_matching.mli4190logplain
-rw-r--r--detyping.ml36577logplain
-rw-r--r--detyping.mli3297logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml60122logplain
-rw-r--r--evarconv.mli3284logplain
-rw-r--r--evardefine.ml7598logplain
-rw-r--r--evardefine.mli1816logplain
-rw-r--r--evarsolve.ml71462logplain
-rw-r--r--evarsolve.mli3384logplain
-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.ml20610logplain
-rw-r--r--glob_ops.mli3765logplain
-rw-r--r--indrec.ml22968logplain
-rw-r--r--indrec.mli2532logplain
-rw-r--r--inductiveops.ml27750logplain
-rw-r--r--inductiveops.mli9543logplain
-rw-r--r--locusops.ml4057logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--ltac_pretype.ml2556logplain
-rw-r--r--miscops.ml2646logplain
-rw-r--r--miscops.mli1254logplain
-rw-r--r--nativenorm.ml17245logplain
-rw-r--r--nativenorm.mli1021logplain
-rw-r--r--patternops.ml18714logplain
-rw-r--r--patternops.mli2070logplain
-rw-r--r--pretype_errors.ml6735logplain
-rw-r--r--pretype_errors.mli5571logplain
-rw-r--r--pretyping.ml48045logplain
-rw-r--r--pretyping.mli4786logplain
-rw-r--r--pretyping.mllib351logplain
-rw-r--r--program.ml3424logplain
-rw-r--r--program.mli1728logplain
-rw-r--r--recordops.ml13254logplain
-rw-r--r--recordops.mli2882logplain
-rw-r--r--redops.ml1735logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml66711logplain
-rw-r--r--reductionops.mli12743logplain
-rw-r--r--retyping.ml10296logplain
-rw-r--r--retyping.mli2002logplain
-rw-r--r--tacred.ml48185logplain
-rw-r--r--tacred.mli3959logplain
-rw-r--r--typeclasses.ml19251logplain
-rw-r--r--typeclasses.mli6034logplain
-rw-r--r--typeclasses_errors.ml1231logplain
-rw-r--r--typeclasses_errors.mli1116logplain
-rw-r--r--typing.ml14727logplain
-rw-r--r--typing.mli2326logplain
-rw-r--r--unification.ml79323logplain
-rw-r--r--unification.mli4316logplain
-rw-r--r--univdecls.ml2584logplain
-rw-r--r--univdecls.mli975logplain
-rw-r--r--vnorm.ml13649logplain
-rw-r--r--vnorm.mli647logplain