/pretyping/

• ../
• arguments_renaming.ml
• arguments_renaming.mli
• cases.ml
• cases.mli
• cbv.ml
• cbv.mli
• classops.ml
• classops.mli
• coercion.ml
• coercion.mli
• constr_matching.ml
• constr_matching.mli
• detyping.ml
• detyping.mli
• doc.tex
• evarconv.ml
• evarconv.mli
• evardefine.ml
• evardefine.mli
• evarsolve.ml
• evarsolve.mli
• find_subterm.ml
• find_subterm.mli
• geninterp.ml
• geninterp.mli
• glob_ops.ml
• glob_ops.mli
• glob_term.ml
• indrec.ml
• indrec.mli
• inductiveops.ml
• inductiveops.mli
• inferCumulativity.ml
• inferCumulativity.mli
• locus.ml
• locusops.ml
• locusops.mli
• ltac_pretype.ml
• miscops.ml
• miscops.mli
• nativenorm.ml
• nativenorm.mli
• pattern.ml
• patternops.ml
• patternops.mli
• pretype_errors.ml
• pretype_errors.mli
• pretyping.ml
• pretyping.mli
• pretyping.mllib
• program.ml
• program.mli
• recordops.ml
• recordops.mli
• reductionops.ml
• reductionops.mli
• retyping.ml
• retyping.mli
• tacred.ml
• tacred.mli
• typeclasses.ml
• typeclasses.mli
• typeclasses_errors.ml
• typeclasses_errors.mli
• typing.ml
• typing.mli
• unification.ml
• unification.mli
• vnorm.ml
• vnorm.mli