summaryrefslogtreecommitdiff
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml65007logplain
-rw-r--r--cases.mli1793logplain
-rw-r--r--cbv.ml13081logplain
-rw-r--r--cbv.mli2033logplain
-rw-r--r--classops.ml11627logplain
-rw-r--r--classops.mli3202logplain
-rw-r--r--clenv.ml15068logplain
-rw-r--r--clenv.mli4278logplain
-rw-r--r--coercion.ml9989logplain
-rw-r--r--coercion.mli2338logplain
-rw-r--r--detyping.ml23750logplain
-rw-r--r--detyping.mli1849logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml17499logplain
-rw-r--r--evarconv.mli1327logplain
-rw-r--r--evarutil.ml24090logplain
-rw-r--r--evarutil.mli5640logplain
-rw-r--r--evd.ml17380logplain
-rw-r--r--evd.mli6032logplain
-rw-r--r--indrec.ml21668logplain
-rw-r--r--indrec.mli2275logplain
-rw-r--r--inductiveops.ml13697logplain
-rw-r--r--inductiveops.mli4595logplain
-rw-r--r--matching.ml9474logplain
-rw-r--r--matching.mli2046logplain
-rw-r--r--pattern.ml9401logplain
-rw-r--r--pattern.mli2583logplain
-rw-r--r--pretype_errors.ml6131logplain
-rw-r--r--pretype_errors.mli3508logplain
-rw-r--r--pretyping.ml25908logplain
-rw-r--r--pretyping.mli3642logplain
-rw-r--r--rawterm.ml9686logplain
-rw-r--r--rawterm.mli4722logplain
-rw-r--r--recordops.ml8100logplain
-rwxr-xr-xrecordops.mli1917logplain
-rw-r--r--reductionops.ml28895logplain
-rw-r--r--reductionops.mli7870logplain
-rw-r--r--retyping.ml6097logplain
-rw-r--r--retyping.mli1530logplain
-rw-r--r--tacred.ml30183logplain
-rw-r--r--tacred.mli2824logplain
-rw-r--r--termops.ml34264logplain
-rw-r--r--termops.mli8298logplain
-rw-r--r--typing.ml6091logplain
-rw-r--r--typing.mli1373logplain
-rw-r--r--unification.ml16600logplain
-rw-r--r--unification.mli1343logplain