Tactics.Internalval explicit_intro_names : 'a Tactypes.intro_pattern_expr CAst.t list -> Names.Id.Set.tval check_name_unicity : Environ.env -> Names.Id.t list -> Names.Id.t list -> 'a Tactypes.intro_pattern_expr CAst.t list -> unitval 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.tacticval clear_wildcards : Names.lident list -> unit Proofview.tacticval 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