aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3629logplain
-rw-r--r--arguments_renaming.mli993logplain
-rw-r--r--cases.ml106163logplain
-rw-r--r--cases.mli4528logplain
-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.ml20852logplain
-rw-r--r--constr_matching.mli4188logplain
-rw-r--r--detyping.ml36578logplain
-rw-r--r--detyping.mli3305logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml60106logplain
-rw-r--r--evarconv.mli3292logplain
-rw-r--r--evardefine.ml7584logplain
-rw-r--r--evardefine.mli1824logplain
-rw-r--r--evarsolve.ml71450logplain
-rw-r--r--evarsolve.mli3382logplain
-rw-r--r--find_subterm.ml6704logplain
-rw-r--r--find_subterm.mli2912logplain
-rw-r--r--glob_ops.ml20604logplain
-rw-r--r--glob_ops.mli3769logplain
-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--ltac_pretype.ml2556logplain
-rw-r--r--miscops.ml2646logplain
-rw-r--r--miscops.mli1254logplain
-rw-r--r--nativenorm.ml17257logplain
-rw-r--r--nativenorm.mli1021logplain
-rw-r--r--patternops.ml18393logplain
-rw-r--r--patternops.mli2070logplain
-rw-r--r--pretype_errors.ml6733logplain
-rw-r--r--pretype_errors.mli5569logplain
-rw-r--r--pretyping.ml47509logplain
-rw-r--r--pretyping.mli4782logplain
-rw-r--r--pretyping.mllib341logplain
-rw-r--r--program.ml3424logplain
-rw-r--r--program.mli1728logplain
-rw-r--r--recordops.ml13277logplain
-rw-r--r--recordops.mli2874logplain
-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.ml48160logplain
-rw-r--r--tacred.mli3959logplain
-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.ml78319logplain
-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