Module Ltac2_plugin.Tac2tactics
val intros_patterns : Tac2types.evars_flag -> Tac2types.intro_pattern list -> unit Proofview.tactic
val apply : Tac2types.advanced_flag -> Tac2types.evars_flag -> Tac2types.constr_with_bindings Tac2types.thunk list -> (Names.Id.t * Tac2types.intro_pattern option) option -> unit Proofview.tactic
val induction_destruct : Tac2expr.rec_flag -> Tac2types.evars_flag -> Tac2types.induction_clause list -> Tac2types.constr_with_bindings option -> unit Proofview.tactic
val elim : Tac2types.evars_flag -> Tac2types.constr_with_bindings -> Tac2types.constr_with_bindings option -> unit Proofview.tactic
val general_case_analysis : Tac2types.evars_flag -> Tac2types.constr_with_bindings -> unit Proofview.tactic
val generalize : (EConstr.constr * Tac2types.occurrences * Names.Name.t) list -> unit Proofview.tactic
val constructor_tac : Tac2types.evars_flag -> int option -> int -> Tac2types.bindings -> unit Proofview.tactic
val left_with_bindings : Tac2types.evars_flag -> Tac2types.bindings -> unit Proofview.tactic
val right_with_bindings : Tac2types.evars_flag -> Tac2types.bindings -> unit Proofview.tactic
val split_with_bindings : Tac2types.evars_flag -> Tac2types.bindings -> unit Proofview.tactic
val specialize : Tac2types.constr_with_bindings -> Tac2types.intro_pattern option -> unit Proofview.tactic
val change : Pattern.constr_pattern option -> (EConstr.constr array, EConstr.constr) Tac2ffi.fun1 -> Tac2types.clause -> unit Proofview.tactic
val rewrite : Tac2types.evars_flag -> Tac2types.rewriting list -> Tac2types.clause -> unit Tac2types.thunk option -> unit Proofview.tactic
val symmetry : Tac2types.clause -> unit Proofview.tactic
val forward : bool -> unit Proofview.tactic option option -> Tac2types.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
val assert_ : Tac2types.assertion -> unit Proofview.tactic
val letin_pat_tac : Tac2types.evars_flag -> (bool * Tac2types.intro_pattern_naming) option -> Names.Name.t -> (Evd.evar_map * EConstr.constr) -> Tac2types.clause -> unit Proofview.tactic
val reduce : Redexpr.red_expr -> Tac2types.clause -> unit Proofview.tactic
val simpl : Names.GlobRef.t Genredexpr.glob_red_flag -> (Pattern.constr_pattern * Tac2types.occurrences) option -> Tac2types.clause -> unit Proofview.tactic
val cbv : Names.GlobRef.t Genredexpr.glob_red_flag -> Tac2types.clause -> unit Proofview.tactic
val cbn : Names.GlobRef.t Genredexpr.glob_red_flag -> Tac2types.clause -> unit Proofview.tactic
val lazy_ : Names.GlobRef.t Genredexpr.glob_red_flag -> Tac2types.clause -> unit Proofview.tactic
val unfold : (Names.GlobRef.t * Tac2types.occurrences) list -> Tac2types.clause -> unit Proofview.tactic
val pattern : (EConstr.constr * Tac2types.occurrences) list -> Tac2types.clause -> unit Proofview.tactic
val vm : (Pattern.constr_pattern * Tac2types.occurrences) option -> Tac2types.clause -> unit Proofview.tactic
val native : (Pattern.constr_pattern * Tac2types.occurrences) option -> Tac2types.clause -> unit Proofview.tactic
val eval_red : EConstr.constr -> EConstr.constr Proofview.tactic
val eval_hnf : EConstr.constr -> EConstr.constr Proofview.tactic
val eval_simpl : Names.GlobRef.t Genredexpr.glob_red_flag -> (Pattern.constr_pattern * Tac2types.occurrences) option -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_cbv : Names.GlobRef.t Genredexpr.glob_red_flag -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_cbn : Names.GlobRef.t Genredexpr.glob_red_flag -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_lazy : Names.GlobRef.t Genredexpr.glob_red_flag -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_unfold : (Names.GlobRef.t * Tac2types.occurrences) list -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_fold : EConstr.constr list -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_pattern : (EConstr.t * Tac2types.occurrences) list -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_vm : (Pattern.constr_pattern * Tac2types.occurrences) option -> EConstr.constr -> EConstr.constr Proofview.tactic
val eval_native : (Pattern.constr_pattern * Tac2types.occurrences) option -> EConstr.constr -> EConstr.constr Proofview.tactic
val discriminate : Tac2types.evars_flag -> Tac2types.destruction_arg option -> unit Proofview.tactic
val injection : Tac2types.evars_flag -> Tac2types.intro_pattern list option -> Tac2types.destruction_arg option -> unit Proofview.tactic
val autorewrite : all:bool -> unit Tac2types.thunk option -> Names.Id.t list -> Tac2types.clause -> unit Proofview.tactic
val trivial : Hints.debug -> EConstr.constr Tac2types.thunk list -> Names.Id.t list option -> unit Proofview.tactic
val auto : Hints.debug -> int option -> EConstr.constr Tac2types.thunk list -> Names.Id.t list option -> unit Proofview.tactic
val eauto : Hints.debug -> int option -> int option -> EConstr.constr Tac2types.thunk list -> Names.Id.t list option -> unit Proofview.tactic
val typeclasses_eauto : Class_tactics.search_strategy option -> int option -> Names.Id.t list option -> unit Proofview.tactic
val unify : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val inversion : Inv.inversion_kind -> Tac2types.destruction_arg -> Tac2types.intro_pattern option -> Names.Id.t list option -> unit Proofview.tactic
val contradiction : Tac2types.constr_with_bindings option -> unit Proofview.tactic