Module `Recdef_plugin.Recdef`

val tclUSER_if_not_mes : Tacmach.tactic -> bool -> Names.Id.t list option -> Tacmach.tactic
val recursive_definition : bool -> Names.Id.t -> Constrintern.internalization_env -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> int -> Constrexpr.constr_expr -> (Constr.pconstant -> Indfun_common.tcc_lemma_value Stdlib.ref -> Constr.pconstant -> Constr.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option