aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
ModeNameSize
-rw-r--r--arguments_renaming.ml3508logplain
-rw-r--r--arguments_renaming.mli1000logplain
-rw-r--r--cases.ml95348logplain
-rw-r--r--cases.mli4245logplain
-rw-r--r--cbv.ml14069logplain
-rw-r--r--cbv.mli2073logplain
-rw-r--r--classops.ml15546logplain
-rw-r--r--classops.mli3600logplain
-rw-r--r--coercion.ml16419logplain
-rw-r--r--coercion.mli2970logplain
-rw-r--r--constrMatching.ml14691logplain
-rw-r--r--constrMatching.mli3876logplain
-rw-r--r--detyping.ml25822logplain
-rw-r--r--detyping.mli3097logplain
-rw-r--r--doc.tex215logplain
-rw-r--r--evarconv.ml37646logplain
-rw-r--r--evarconv.mli2757logplain
-rw-r--r--evarsolve.ml56307logplain
-rw-r--r--evarsolve.mli2574logplain
-rw-r--r--evarutil.ml29096logplain
-rw-r--r--evarutil.mli7665logplain
-rw-r--r--evd.ml32743logplain
-rw-r--r--evd.mli14169logplain
-rw-r--r--glob_ops.ml13855logplain
-rw-r--r--glob_ops.mli1869logplain
-rw-r--r--indrec.ml19951logplain
-rw-r--r--indrec.mli2367logplain
-rw-r--r--inductiveops.ml17635logplain
-rw-r--r--inductiveops.mli6046logplain
-rw-r--r--locusops.ml2773logplain
-rw-r--r--locusops.mli1319logplain
-rw-r--r--miscops.ml1244logplain
-rw-r--r--miscops.mli786logplain
-rw-r--r--namegen.ml11919logplain
-rw-r--r--namegen.mli3537logplain
-rw-r--r--nativenorm.ml13070logplain
-rw-r--r--nativenorm.mli778logplain
-rw-r--r--patternops.ml15115logplain
-rw-r--r--patternops.mli2022logplain
-rw-r--r--pretype_errors.ml5491logplain
-rw-r--r--pretype_errors.mli4551logplain
-rw-r--r--pretyping.ml30675logplain
-rw-r--r--pretyping.mli4717logplain
-rw-r--r--pretyping.mllib332logplain
-rw-r--r--program.ml2580logplain
-rw-r--r--program.mli1229logplain
-rw-r--r--recordops.ml11580logplain
-rw-r--r--recordops.mli2718logplain
-rw-r--r--redops.ml1521logplain
-rw-r--r--redops.mli634logplain
-rw-r--r--reductionops.ml44521logplain
-rw-r--r--reductionops.mli10278logplain
-rw-r--r--retyping.ml8711logplain
-rw-r--r--retyping.mli1903logplain
-rw-r--r--tacred.ml37982logplain
-rw-r--r--tacred.mli3422logplain
-rw-r--r--term_dnet.ml12152logplain
-rw-r--r--term_dnet.mli2637logplain
-rw-r--r--termops.ml38425logplain
-rw-r--r--termops.mli11533logplain
-rw-r--r--typeclasses.ml16574logplain
-rw-r--r--typeclasses.mli4982logplain
-rw-r--r--typeclasses_errors.ml1968logplain
-rw-r--r--typeclasses_errors.mli1587logplain
-rw-r--r--typing.ml10298logplain
-rw-r--r--typing.mli1546logplain
-rw-r--r--unification.ml48973logplain
-rw-r--r--unification.mli3033logplain
-rw-r--r--vnorm.ml10591logplain
-rw-r--r--vnorm.mli655logplain