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

val with_strategy : 
  Conv_oracle.level ->
  Names.GlobRef.t list ->
  'a Tac2types.thunk ->
  'a 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

val wrap_tactic_call : 
  (EConstr.constr ->
    EConstr.constr ->
    EConstr.constr option ->
    Rewrite.Result.t Proofview.tactic) ->
  Rewrite.strategy