Module `Ltac2_plugin.Tac2tactics`Source

Local reimplementations of tactics variants from Rocq

val intros_patterns : 
  Tac2types.evars_flag ->
  Tac2types.intro_pattern list ->
  unit Proofview.tactic

Source

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

Source

val induction_destruct : 
  Tac2expr.rec_flag ->
  Tac2types.evars_flag ->
  Tac2types.induction_clause list ->
  Tac2types.constr_with_bindings option ->
  unit Proofview.tactic

Source

val elim : 
  Tac2types.evars_flag ->
  Tac2types.constr_with_bindings ->
  Tac2types.constr_with_bindings option ->
  unit Proofview.tactic

Source

val general_case_analysis : 
  Tac2types.evars_flag ->
  Tac2types.constr_with_bindings ->
  unit Proofview.tactic

Source

val generalize : 
  (EConstr.constr * Tac2types.occurrences * Names.Name.t) list ->
  unit Proofview.tactic

Source

val constructor_tac : 
  Tac2types.evars_flag ->
  int option ->
  int ->
  Tac2types.bindings ->
  unit Proofview.tactic

Source

val left_with_bindings : 
  Tac2types.evars_flag ->
  Tac2types.bindings ->
  unit Proofview.tactic

Source

val right_with_bindings : 
  Tac2types.evars_flag ->
  Tac2types.bindings ->
  unit Proofview.tactic

Source

val split_with_bindings : 
  Tac2types.evars_flag ->
  Tac2types.bindings ->
  unit Proofview.tactic

Source

val specialize : 
  Tac2types.constr_with_bindings ->
  Tac2types.intro_pattern option ->
  unit Proofview.tactic

Source

val change : 
  Pattern.constr_pattern option ->
  (EConstr.constr array, EConstr.constr) Tac2ffi.fun1 ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

val rewrite : 
  Tac2types.evars_flag ->
  Tac2types.rewriting list ->
  Tac2types.clause ->
  unit Tac2types.thunk option ->
  unit Proofview.tactic

Source

val setoid_rewrite : 
  Tac2types.orientation ->
  Tac2types.constr_with_bindings Proofview.tactic ->
  Tac2types.occurrences ->
  Names.Id.t option ->
  unit Proofview.tactic

Sourceval symmetry : Tac2types.clause -> unit Proofview.tactic

Source

val forward : 
  bool ->
  unit Proofview.tactic option option ->
  Tac2types.intro_pattern option ->
  EConstr.constr ->
  unit Proofview.tactic

Sourceval assert_ : Tac2types.assertion -> unit Proofview.tactic

Source

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

Sourceval reduce : Redexpr.red_expr -> Tac2types.clause -> unit Proofview.tactic

Source

val simpl : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  (Pattern.constr_pattern * Tac2types.occurrences) option ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

val cbv : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

val cbn : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

val lazy_ : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

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

Source

val pattern : 
  (EConstr.constr * Tac2types.occurrences) list ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

val vm : 
  (Pattern.constr_pattern * Tac2types.occurrences) option ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

val native : 
  (Pattern.constr_pattern * Tac2types.occurrences) option ->
  Tac2types.clause ->
  unit Proofview.tactic

Sourceval eval_red : EConstr.constr -> EConstr.constr Proofview.tactic

Sourceval eval_hnf : EConstr.constr -> EConstr.constr Proofview.tactic

Source

val eval_simpl : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  (Pattern.constr_pattern * Tac2types.occurrences) option ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_cbv : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_cbn : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_lazy : 
  Names.GlobRef.t Genredexpr.glob_red_flag ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_unfold : 
  (Names.GlobRef.t * Tac2types.occurrences) list ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_fold : 
  EConstr.constr list ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_pattern : 
  (EConstr.t * Tac2types.occurrences) list ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_vm : 
  (Pattern.constr_pattern * Tac2types.occurrences) option ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val eval_native : 
  (Pattern.constr_pattern * Tac2types.occurrences) option ->
  EConstr.constr ->
  EConstr.constr Proofview.tactic

Source

val discriminate : 
  Tac2types.evars_flag ->
  Tac2types.destruction_arg option ->
  unit Proofview.tactic

Source

val injection : 
  Tac2types.evars_flag ->
  Tac2types.intro_pattern list option ->
  Tac2types.destruction_arg option ->
  unit Proofview.tactic

Source

val autorewrite : 
  all:bool ->
  unit Tac2types.thunk option ->
  Names.Id.t list ->
  Tac2types.clause ->
  unit Proofview.tactic

Source

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

Source

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

Source

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

Source

val typeclasses_eauto : 
  Class_tactics.search_strategy option ->
  int option ->
  Names.Id.t list option ->
  unit Proofview.tactic

Sourceval unify : EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Source

val inversion : 
  Inv.inversion_kind ->
  Tac2types.destruction_arg ->
  Tac2types.intro_pattern option ->
  Names.Id.t list option ->
  unit Proofview.tactic

Source

val contradiction : 
  Tac2types.constr_with_bindings option ->
  unit Proofview.tactic

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

Source

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

Internal

Sourceval mk_intro_pattern : Tac2types.intro_pattern -> Tactypes.intro_pattern

Source

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

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2tactics/index.html

Module `Ltac2_plugin.Tac2tactics`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2tactics/index.html

Module Ltac2_plugin.Tac2tacticsSource

Module `Ltac2_plugin.Tac2tactics`Source