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