Module `Tactics.Internal`

val explicit_intro_names : 'a Tactypes.intro_pattern_expr CAst.t list -> Names.Id.Set.t
val check_name_unicity : Environ.env -> Names.Id.t list -> Names.Id.t list -> 'a Tactypes.intro_pattern_expr CAst.t list -> unit
val clear_gen : (Environ.env -> Evd.evar_map -> Names.Id.t -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> Evd.evar_map * Environ.named_context_val * EConstr.types) -> Names.Id.t list -> unit Proofview.tactic
val clear_wildcards : Names.lident list -> unit Proofview.tactic
val dest_intro_patterns : evars_flag -> Names.Id.Set.t -> Names.lident list -> Names.Id.t Logic.move_location -> Tactypes.intro_patterns -> (Names.Id.t list -> Names.lident list -> unit Proofview.tactic) -> unit Proofview.tactic