aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3629logplain
-rw-r--r--arguments_renaming.mli993logplain
-rw-r--r--cases.ml105804logplain
-rw-r--r--cases.mli4515logplain
-rw-r--r--cbv.ml17254logplain
-rw-r--r--cbv.mli2166logplain
-rw-r--r--classops.ml17280logplain
-rw-r--r--classops.mli3775logplain
-rw-r--r--coercion.ml18693logplain
-rw-r--r--coercion.mli2979logplain
-rw-r--r--constr_matching.ml20615logplain
-rw-r--r--constr_matching.mli4170logplain
-rw-r--r--detyping.ml35694logplain
-rw-r--r--detyping.mli3240logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml59845logplain
-rw-r--r--evarconv.mli3292logplain
-rw-r--r--evardefine.ml7570logplain
-rw-r--r--evardefine.mli1833logplain
-rw-r--r--evarsolve.ml70801logplain
-rw-r--r--evarsolve.mli3382logplain
-rw-r--r--find_subterm.ml6704logplain
-rw-r--r--find_subterm.mli2912logplain
-rw-r--r--glob_ops.ml20426logplain
-rw-r--r--glob_ops.mli3670logplain
-rw-r--r--indrec.ml22985logplain
-rw-r--r--indrec.mli2527logplain
-rw-r--r--inductiveops.ml27756logplain
-rw-r--r--inductiveops.mli9550logplain
-rw-r--r--locusops.ml4057logplain
-rw-r--r--locusops.mli1625logplain
-rw-r--r--miscops.ml2646logplain
-rw-r--r--miscops.mli1254logplain
-rw-r--r--nativenorm.ml15062logplain
-rw-r--r--nativenorm.mli852logplain
-rw-r--r--patternops.ml17072logplain
-rw-r--r--patternops.mli1999logplain
-rw-r--r--pretype_errors.ml6733logplain
-rw-r--r--pretype_errors.mli5569logplain
-rw-r--r--pretyping.ml49823logplain
-rw-r--r--pretyping.mli5769logplain
-rw-r--r--pretyping.mllib318logplain
-rw-r--r--program.ml3424logplain
-rw-r--r--program.mli1728logplain
-rw-r--r--recordops.ml12628logplain
-rw-r--r--recordops.mli2869logplain
-rw-r--r--redops.ml1735logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml66853logplain
-rw-r--r--reductionops.mli12802logplain
-rw-r--r--retyping.ml10617logplain
-rw-r--r--retyping.mli2017logplain
-rw-r--r--tacred.ml47838logplain
-rw-r--r--tacred.mli3941logplain
-rw-r--r--typeclasses.ml18621logplain
-rw-r--r--typeclasses.mli5860logplain
-rw-r--r--typeclasses_errors.ml1231logplain
-rw-r--r--typeclasses_errors.mli1116logplain
-rw-r--r--typing.ml15171logplain
-rw-r--r--typing.mli2322logplain
-rw-r--r--unification.ml78191logplain
-rw-r--r--unification.mli4314logplain
-rw-r--r--vnorm.ml13657logplain
-rw-r--r--vnorm.mli647logplain