Module Inv
type inversion_status=|Dep of EConstr.constr option|NoDeptype inversion_kind=|SimpleInversion|FullInversion|FullInversionClear
val inv_clause : inversion_kind -> Tactypes.or_and_intro_pattern option -> Names.Id.t list -> Tactypes.quantified_hypothesis -> unit Proofview.tacticval inv : inversion_kind -> Tactypes.or_and_intro_pattern option -> Tactypes.quantified_hypothesis -> unit Proofview.tacticval dinv : inversion_kind -> EConstr.constr option -> Tactypes.or_and_intro_pattern option -> Tactypes.quantified_hypothesis -> unit Proofview.tacticval inv_tac : Names.Id.t -> unit Proofview.tacticval inv_clear_tac : Names.Id.t -> unit Proofview.tacticval dinv_tac : Names.Id.t -> unit Proofview.tacticval dinv_clear_tac : Names.Id.t -> unit Proofview.tactic