aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3629logplain
-rw-r--r--arguments_renaming.mli993logplain
-rw-r--r--cases.ml106142logplain
-rw-r--r--cases.mli4511logplain
-rw-r--r--cbv.ml17254logplain
-rw-r--r--cbv.mli2166logplain
-rw-r--r--classops.ml17283logplain
-rw-r--r--classops.mli3749logplain
-rw-r--r--coercion.ml18690logplain
-rw-r--r--coercion.mli2979logplain
-rw-r--r--constr_matching.ml20831logplain
-rw-r--r--constr_matching.mli4170logplain
-rw-r--r--detyping.ml36560logplain
-rw-r--r--detyping.mli3287logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml59807logplain
-rw-r--r--evarconv.mli3292logplain
-rw-r--r--evardefine.ml7584logplain
-rw-r--r--evardefine.mli1824logplain
-rw-r--r--evarsolve.ml70658logplain
-rw-r--r--evarsolve.mli3382logplain
-rw-r--r--find_subterm.ml6704logplain
-rw-r--r--find_subterm.mli2912logplain
-rw-r--r--glob_ops.ml20586logplain
-rw-r--r--glob_ops.mli3763logplain
-rw-r--r--indrec.ml22985logplain
-rw-r--r--indrec.mli2527logplain
-rw-r--r--inductiveops.ml27751logplain
-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.ml17257logplain
-rw-r--r--nativenorm.mli1021logplain
-rw-r--r--patternops.ml17385logplain
-rw-r--r--patternops.mli1999logplain
-rw-r--r--pretype_errors.ml6733logplain
-rw-r--r--pretype_errors.mli5569logplain
-rw-r--r--pretyping.ml47490logplain
-rw-r--r--pretyping.mli4764logplain
-rw-r--r--pretyping.mllib328logplain
-rw-r--r--program.ml3424logplain
-rw-r--r--program.mli1728logplain
-rw-r--r--recordops.ml12782logplain
-rw-r--r--recordops.mli2859logplain
-rw-r--r--redops.ml1735logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml66536logplain
-rw-r--r--reductionops.mli12739logplain
-rw-r--r--retyping.ml10291logplain
-rw-r--r--retyping.mli2008logplain
-rw-r--r--tacred.ml48157logplain
-rw-r--r--tacred.mli3941logplain
-rw-r--r--typeclasses.ml19237logplain
-rw-r--r--typeclasses.mli6030logplain
-rw-r--r--typeclasses_errors.ml1231logplain
-rw-r--r--typeclasses_errors.mli1116logplain
-rw-r--r--typing.ml14727logplain
-rw-r--r--typing.mli2322logplain
-rw-r--r--unification.ml78207logplain
-rw-r--r--unification.mli4314logplain
-rw-r--r--univdecls.ml2594logplain
-rw-r--r--univdecls.mli975logplain
-rw-r--r--vnorm.ml13653logplain
-rw-r--r--vnorm.mli647logplain