Tac2tactics (coq-core.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 option * 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 ->
  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