aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--cases.ml62298logplain
-rw-r--r--cases.mli1622logplain
-rw-r--r--cbv.ml13413logplain
-rw-r--r--cbv.mli2006logplain
-rw-r--r--classops.ml11581logplain
-rw-r--r--classops.mli3152logplain
-rw-r--r--clenv.ml15023logplain
-rw-r--r--clenv.mli4231logplain
-rw-r--r--coercion.ml10325logplain
-rw-r--r--coercion.mli2618logplain
-rw-r--r--detyping.ml23693logplain
-rw-r--r--detyping.mli2201logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml17450logplain
-rw-r--r--evarconv.mli1279logplain
-rw-r--r--evarutil.ml24069logplain
-rw-r--r--evarutil.mli5591logplain
-rw-r--r--evd.ml17252logplain
-rw-r--r--evd.mli5935logplain
-rw-r--r--indrec.ml21632logplain
-rw-r--r--indrec.mli2227logplain
-rw-r--r--inductiveops.ml14895logplain
-rw-r--r--inductiveops.mli4802logplain
-rw-r--r--matching.ml10185logplain
-rw-r--r--matching.mli1996logplain
-rw-r--r--pattern.ml11089logplain
-rw-r--r--pattern.mli2687logplain
-rw-r--r--pretype_errors.ml6077logplain
-rw-r--r--pretype_errors.mli3453logplain
-rw-r--r--pretyping.ml25958logplain
-rw-r--r--pretyping.mli3592logplain
-rw-r--r--rawterm.ml10001logplain
-rw-r--r--rawterm.mli4980logplain
-rw-r--r--recordops.ml8053logplain
-rwxr-xr-xrecordops.mli1866logplain
-rw-r--r--reductionops.ml28767logplain
-rw-r--r--reductionops.mli8405logplain
-rw-r--r--retyping.ml5798logplain
-rw-r--r--retyping.mli1491logplain
-rw-r--r--tacred.ml30136logplain
-rw-r--r--tacred.mli2775logplain
-rw-r--r--termops.ml34213logplain
-rw-r--r--termops.mli8246logplain
-rw-r--r--typing.ml5458logplain
-rw-r--r--typing.mli1327logplain
-rw-r--r--unification.ml16551logplain
-rw-r--r--unification.mli1290logplain