Module Tactics

General functions.
val is_quantified_hypothesis : Names.Id.t -> Proofview.Goal.t -> bool
Primitive tactics.
exception NotConvertible
val introduction : Names.Id.t -> unit Proofview.tactic
val convert_concl : cast:bool -> check:bool -> EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
val convert_hyp : check:bool -> reorder:bool -> EConstr.named_declaration -> unit Proofview.tactic
val mutual_fix : Names.Id.t -> int -> (Names.Id.t * int * EConstr.constr) list -> int -> unit Proofview.tactic
val fix : Names.Id.t -> int -> unit Proofview.tactic
val mutual_cofix : Names.Id.t -> (Names.Id.t * EConstr.constr) list -> int -> unit Proofview.tactic
val cofix : Names.Id.t -> unit Proofview.tactic
val convert : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val convert_leq : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
Introduction tactics.
val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
val find_intro_names : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Names.Id.t list
val intro : unit Proofview.tactic
val introf : unit Proofview.tactic
val intro_move : Names.Id.t option -> Names.Id.t Logic.move_location -> unit Proofview.tactic
val intro_move_avoid : Names.Id.t option -> Names.Id.Set.t -> Names.Id.t Logic.move_location -> unit Proofview.tactic
val intros_move : (Names.Id.t * Names.Id.t Logic.move_location) list -> unit Proofview.tactic
val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic

intro_avoiding idl acts as intro but prevents the new Id.t to belong to idl

val intro_replacing : Names.Id.t -> unit Proofview.tactic
val intro_using : Names.Id.t -> unit Proofview.tactic
val intro_using_then : Names.Id.t -> (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
val intros_mustbe_force : Names.Id.t list -> unit Proofview.tactic
val intro_then : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val intros_using : Names.Id.t list -> unit Proofview.tactic
val intros_using_then : Names.Id.t list -> (Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic
val intros_replacing : Names.Id.t list -> unit Proofview.tactic
val intros_possibly_replacing : Names.Id.t list -> unit Proofview.tactic
val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic

auto_intros_tac names handles Automatic Introduction of binders

val intros : unit Proofview.tactic
val intros_until : Tactypes.quantified_hypothesis -> unit Proofview.tactic
val intros_clearing : bool list -> unit Proofview.tactic
val try_intros_until : (Names.Id.t -> unit Proofview.tactic) -> Tactypes.quantified_hypothesis -> unit Proofview.tactic
type evars_flag = bool
type rec_flag = bool
type advanced_flag = bool
type clear_flag = bool option
type 'a core_destruction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of Names.lident
| ElimOnAnonHyp of int
type 'a destruction_arg = clear_flag * 'a core_destruction_arg
val onInductionArg : (clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic) -> EConstr.constr Tactypes.with_bindings destruction_arg -> unit Proofview.tactic
val force_destruction_arg : evars_flag -> Environ.env -> Evd.evar_map -> Tactypes.delayed_open_constr_with_bindings destruction_arg -> Evd.evar_map * EConstr.constr Tactypes.with_bindings destruction_arg
val finish_evar_resolution : ?⁠flags:Pretyping.inference_flags -> Environ.env -> Evd.evar_map -> (Evd.evar_map option * EConstr.constr) -> Evd.evar_map * EConstr.constr
val use_clear_hyp_by_default : unit -> bool
Introduction tactics with eliminations.
val intro_patterns : evars_flag -> Tactypes.intro_patterns -> unit Proofview.tactic
val intro_patterns_to : evars_flag -> Names.Id.t Logic.move_location -> Tactypes.intro_patterns -> unit Proofview.tactic
val intro_patterns_bound_to : evars_flag -> int -> Names.Id.t Logic.move_location -> Tactypes.intro_patterns -> unit Proofview.tactic
val intro_pattern_to : evars_flag -> Names.Id.t Logic.move_location -> Tactypes.delayed_open_constr Tactypes.intro_pattern_expr -> unit Proofview.tactic
val intros_patterns : evars_flag -> Tactypes.intro_patterns -> unit Proofview.tactic

Implements user-level "intros", with standing for "**"

Exact tactics.
val assumption : unit Proofview.tactic
val exact_no_check : EConstr.constr -> unit Proofview.tactic
val vm_cast_no_check : EConstr.constr -> unit Proofview.tactic
val native_cast_no_check : EConstr.constr -> unit Proofview.tactic
val exact_check : EConstr.constr -> unit Proofview.tactic
val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic
Reduction tactics.
type tactic_reduction = Reductionops.reduction_function
type e_tactic_reduction = Reductionops.e_reduction_function
type change_arg = Ltac_pretype.patvar_map -> Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.constr
val make_change_arg : EConstr.constr -> change_arg
val reduct_in_hyp : check:bool -> reorder:bool -> tactic_reduction -> Locus.hyp_location -> unit Proofview.tactic
val reduct_option : check:bool -> (tactic_reduction * Constr.cast_kind) -> Locus.goal_location -> unit Proofview.tactic
val reduct_in_concl : cast:bool -> check:bool -> (tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
val e_reduct_in_concl : cast:bool -> check:bool -> (e_tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
val change_in_concl : check:bool -> (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> unit Proofview.tactic
val change_concl : EConstr.constr -> unit Proofview.tactic
val change_in_hyp : check:bool -> (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> Locus.hyp_location -> unit Proofview.tactic
val red_in_concl : unit Proofview.tactic
val red_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val red_option : Locus.goal_location -> unit Proofview.tactic
val hnf_in_concl : unit Proofview.tactic
val hnf_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val hnf_option : Locus.goal_location -> unit Proofview.tactic
val simpl_in_concl : unit Proofview.tactic
val simpl_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val simpl_option : Locus.goal_location -> unit Proofview.tactic
val normalise_in_concl : unit Proofview.tactic
val normalise_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val normalise_option : Locus.goal_location -> unit Proofview.tactic
val normalise_vm_in_concl : unit Proofview.tactic
val unfold_in_concl : (Locus.occurrences * Tacred.evaluable_global_reference) list -> unit Proofview.tactic
val unfold_in_hyp : (Locus.occurrences * Tacred.evaluable_global_reference) list -> Locus.hyp_location -> unit Proofview.tactic
val unfold_option : (Locus.occurrences * Tacred.evaluable_global_reference) list -> Locus.goal_location -> unit Proofview.tactic
val change : check:bool -> Pattern.constr_pattern option -> change_arg -> Locus.clause -> unit Proofview.tactic
val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic
val reduce : Redexpr.red_expr -> Locus.clause -> unit Proofview.tactic
val unfold_constr : Names.GlobRef.t -> unit Proofview.tactic
Modification of the local context.
val clear : Names.Id.t list -> unit Proofview.tactic
val clear_body : Names.Id.t list -> unit Proofview.tactic
val unfold_body : Names.Id.t -> unit Proofview.tactic
val keep : Names.Id.t list -> unit Proofview.tactic
val apply_clear_request : clear_flag -> bool -> Names.Id.t option -> unit Proofview.tactic
val specialize : EConstr.constr Tactypes.with_bindings -> Tactypes.intro_pattern option -> unit Proofview.tactic
val move_hyp : Names.Id.t -> Names.Id.t Logic.move_location -> unit Proofview.tactic
val rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic
Resolution tactics.
val apply_type : typecheck:bool -> EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
val apply : EConstr.constr -> unit Proofview.tactic
val eapply : ?⁠with_classes:bool -> EConstr.constr -> unit Proofview.tactic
val apply_with_bindings_gen : ?⁠with_classes:bool -> advanced_flag -> evars_flag -> (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list -> unit Proofview.tactic
val apply_with_delayed_bindings_gen : advanced_flag -> evars_flag -> (clear_flag * Tactypes.delayed_open_constr_with_bindings CAst.t) list -> unit Proofview.tactic
val apply_with_bindings : EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val eapply_with_bindings : ?⁠with_classes:bool -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val cut_and_apply : EConstr.constr -> unit Proofview.tactic
val apply_in : advanced_flag -> evars_flag -> Names.Id.t -> (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list -> Tactypes.intro_pattern option -> unit Proofview.tactic
val apply_delayed_in : advanced_flag -> evars_flag -> Names.Id.t -> (clear_flag * Tactypes.delayed_open_constr_with_bindings CAst.t) list -> Tactypes.intro_pattern option -> unit Proofview.tactic -> unit Proofview.tactic
Elimination tactics.
val general_elim_clause : evars_flag -> Unification.unify_flags -> Names.Id.t option -> ((Constr.metavariable * Evd.clbinding) list * EConstr.t * EConstr.types) -> Names.Constant.t -> unit Proofview.tactic
val default_elim : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val simplest_elim : EConstr.constr -> unit Proofview.tactic
val elim : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> EConstr.constr Tactypes.with_bindings option -> unit Proofview.tactic
Case analysis tactics.
val general_case_analysis : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val simplest_case : EConstr.constr -> unit Proofview.tactic
Eliminations giving the type instead of the proof.
val exfalso : unit Proofview.tactic
Constructor tactics.
val constructor_tac : evars_flag -> int option -> int -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val any_constructor : evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic
val one_constructor : int -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val left : EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val right : EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val split : EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val left_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val right_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val split_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings list -> unit Proofview.tactic
val split_with_delayed_bindings : evars_flag -> EConstr.constr Tactypes.bindings Tactypes.delayed_open list -> unit Proofview.tactic
val simplest_left : unit Proofview.tactic
val simplest_right : unit Proofview.tactic
val simplest_split : unit Proofview.tactic
Equality tactics.
val setoid_reflexivity : unit Proofview.tactic Hook.t
val reflexivity_red : bool -> unit Proofview.tactic
val reflexivity : unit Proofview.tactic
val intros_reflexivity : unit Proofview.tactic
val setoid_symmetry : unit Proofview.tactic Hook.t
val symmetry_red : bool -> unit Proofview.tactic
val symmetry : unit Proofview.tactic
val setoid_symmetry_in : (Names.Id.t -> unit Proofview.tactic) Hook.t
val intros_symmetry : Locus.clause -> unit Proofview.tactic
val setoid_transitivity : (EConstr.constr option -> unit Proofview.tactic) Hook.t
val transitivity_red : bool -> EConstr.constr option -> unit Proofview.tactic
val transitivity : EConstr.constr -> unit Proofview.tactic
val etransitivity : unit Proofview.tactic
val intros_transitivity : EConstr.constr option -> unit Proofview.tactic
Cut tactics.
val assert_before_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
val assert_after_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
val assert_before : Names.Name.t -> EConstr.types -> unit Proofview.tactic
val assert_after : Names.Name.t -> EConstr.types -> unit Proofview.tactic
val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic
val enough_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic
val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
val forward : bool -> unit Proofview.tactic option option -> Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
val cut : EConstr.types -> unit Proofview.tactic
Tactics for adding local definitions.
val pose_tac : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
val letin_tac : (bool * Tactypes.intro_pattern_naming) option -> Names.Name.t -> EConstr.constr -> EConstr.types option -> Locus.clause -> unit Proofview.tactic
val letin_pat_tac : evars_flag -> (bool * Tactypes.intro_pattern_naming) option -> Names.Name.t -> (Evd.evar_map option * EConstr.constr) -> Locus.clause -> unit Proofview.tactic
Other tactics.
val constr_eq : strict:bool -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Syntactic equality up to universes. With strict the universe constraints must be already true to succeed, without strict they are added to the evar map.

val unify : ?⁠state:TransparentState.t -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val evarconv_unify : ?⁠state:TransparentState.t -> ?⁠with_ho:bool -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val specialize_eqs : Names.Id.t -> unit Proofview.tactic
val general_rewrite_clause : (bool -> evars_flag -> EConstr.constr Tactypes.with_bindings -> Locus.clause -> unit Proofview.tactic) Hook.t
val subst_one : (bool -> Names.Id.t -> (Names.Id.t * EConstr.constr * bool) -> unit Proofview.tactic) Hook.t
val declare_intro_decomp_eq : ((int -> unit Proofview.tactic) -> (Coqlib.coq_eq_data * EConstr.types * (EConstr.types * EConstr.constr * EConstr.constr)) -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic) -> unit
val with_set_strategy : (Conv_oracle.level * Names.GlobRef.t list) list -> 'a Proofview.tactic -> 'a Proofview.tactic

Tactic analogous to the Strategy vernacular, but only applied locally to the tactic argument

Simple form of basic tactics.
module Simple : sig ... end
Tacticals defined directly in term of Proofview
val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic

refine ~typecheck c is Refine.refine ~typecheck c followed by beta-iota-reduction of the conclusion.

val reduce_after_refine : unit Proofview.tactic

The reducing tactic called after refine.

Internals, do not use
module Internal : sig ... end