Tac2tactics (rocq-runtime.Ltac2

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 setoid_rewrite : Tac2types.orientation -> Tac2types.constr_with_bindings Proofview.tactic -> Tac2types.occurrences -> Names.Id.t option -> unit Proofview.tactic

val rewrite_strat : Rewrite.strategy -> Names.Id.t option -> unit Proofview.tactic

module RewriteStrats : sig ... end

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 option * EConstr.constr) -> Tac2types.clause -> unit Proofview.tactic

val reduce_in : Redexpr.red_expr -> Tac2types.clause -> unit Proofview.tactic

val reduce_constr : Redexpr.red_expr -> EConstr.constr -> EConstr.constr Proofview.tactic

val simpl : Tac2types.red_flag -> Tac2types.red_context -> Redexpr.red_expr Proofview.tactic

val cbv : Tac2types.red_flag -> Redexpr.red_expr Proofview.tactic

val cbn : Names.GlobRef.t Genredexpr.glob_red_flag -> Redexpr.red_expr Proofview.tactic

val lazy_ : Names.GlobRef.t Genredexpr.glob_red_flag -> Redexpr.red_expr Proofview.tactic

val unfold : (Names.GlobRef.t * Tac2types.occurrences) list -> Redexpr.red_expr Proofview.tactic

val pattern : (EConstr.constr * Tac2types.occurrences) list -> Redexpr.red_expr

val vm : Tac2types.red_context -> Redexpr.red_expr

val native : Tac2types.red_context -> Redexpr.red_expr

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 -> Names.GlobRef.t list -> Names.Id.t list option -> unit Proofview.tactic

val auto : Hints.debug -> int option -> Names.GlobRef.t list -> Names.Id.t list option -> unit Proofview.tactic

val eauto : Hints.debug -> int option -> Names.GlobRef.t 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

val current_transparent_state : unit -> TransparentState.t Proofview.tactic

val evarconv_unify : TransparentState.t -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Internal

val mk_intro_pattern : Tac2types.intro_pattern -> Tactypes.intro_pattern

val congruence : int option -> EConstr.constr list option -> unit Proofview.tactic

val simple_congruence : int option -> EConstr.constr list option -> unit Proofview.tactic

val f_equal : unit Proofview.tactic