aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3592logplain
-rw-r--r--arguments_renaming.mli1003logplain
-rw-r--r--cases.ml96210logplain
-rw-r--r--cases.mli4198logplain
-rw-r--r--cbv.ml14480logplain
-rw-r--r--cbv.mli2150logplain
-rw-r--r--classops.ml16960logplain
-rw-r--r--classops.mli3682logplain
-rw-r--r--coercion.ml17729logplain
-rw-r--r--coercion.mli2935logplain
-rw-r--r--constrMatching.ml15600logplain
-rw-r--r--constrMatching.mli3863logplain
-rw-r--r--detyping.ml26580logplain
-rw-r--r--detyping.mli3077logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml43208logplain
-rw-r--r--evarconv.mli2789logplain
-rw-r--r--evarsolve.ml62165logplain
-rw-r--r--evarsolve.mli2837logplain
-rw-r--r--evarutil.ml30159logplain
-rw-r--r--evarutil.mli9030logplain
-rw-r--r--evd.ml53801logplain
-rw-r--r--evd.mli20000logplain
-rw-r--r--find_subterm.ml5601logplain
-rw-r--r--find_subterm.mli2843logplain
-rw-r--r--glob_ops.ml14087logplain
-rw-r--r--glob_ops.mli1769logplain
-rw-r--r--indrec.ml20599logplain
-rw-r--r--indrec.mli2346logplain
-rw-r--r--inductiveops.ml19518logplain
-rw-r--r--inductiveops.mli6233logplain
-rw-r--r--locusops.ml2773logplain
-rw-r--r--locusops.mli1304logplain
-rw-r--r--miscops.ml1244logplain
-rw-r--r--miscops.mli786logplain
-rw-r--r--namegen.ml12908logplain
-rw-r--r--namegen.mli3952logplain
-rw-r--r--nativenorm.ml13652logplain
-rw-r--r--nativenorm.mli752logplain
-rw-r--r--patternops.ml15583logplain
-rw-r--r--patternops.mli1977logplain
-rw-r--r--pretype_errors.ml5736logplain
-rw-r--r--pretype_errors.mli4779logplain
-rw-r--r--pretyping.ml34419logplain
-rw-r--r--pretyping.mli4791logplain
-rw-r--r--pretyping.mllib335logplain
-rw-r--r--program.ml2703logplain
-rw-r--r--program.mli1532logplain
-rw-r--r--recordops.ml11953logplain
-rw-r--r--recordops.mli2728logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml56454logplain
-rw-r--r--reductionops.mli11435logplain
-rw-r--r--retyping.ml9390logplain
-rw-r--r--retyping.mli1865logplain
-rw-r--r--tacred.ml43395logplain
-rw-r--r--tacred.mli3715logplain
-rw-r--r--termops.ml33605logplain
-rw-r--r--termops.mli9814logplain
-rw-r--r--typeclasses.ml18597logplain
-rw-r--r--typeclasses.mli5420logplain
-rw-r--r--typeclasses_errors.ml1964logplain
-rw-r--r--typeclasses_errors.mli1535logplain
-rw-r--r--typing.ml10552logplain
-rw-r--r--typing.mli1601logplain
-rw-r--r--unification.ml60794logplain
-rw-r--r--unification.mli4087logplain
-rw-r--r--vnorm.ml10892logplain
-rw-r--r--vnorm.mli629logplain