package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val is_quantified_hypothesis : Names.Id.t -> Proofview.Goal.t -> bool
val introduction : Names.Id.t -> unit Proofview.tactic
val convert_concl : check:bool -> EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
val convert_hyp : check:bool -> reorder:bool -> EConstr.named_declaration -> unit Proofview.tactic
val convert_concl_no_check : EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
  • deprecated use [Tactics.convert_concl]
val convert_hyp_no_check : EConstr.named_declaration -> unit Proofview.tactic
  • deprecated use [Tactics.convert_hyp]
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_leq : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
val find_intro_names : EConstr.rel_context -> Goal.goal Evd.sigma -> 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 intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic
val intro_replacing : Names.Id.t -> unit Proofview.tactic
val intro_using : Names.Id.t -> unit Proofview.tactic
  • deprecated Prefer [intro_using_then] to avoid renaming issues.
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
  • deprecated Prefer [intros_using_then] to avoid renaming issues.
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
val intros : unit Proofview.tactic
val depth_of_quantified_hypothesis : bool -> Tactypes.quantified_hypothesis -> Proofview.Goal.t -> int
val intros_clearing : bool list -> 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 =
  1. | ElimOnConstr of 'a
  2. | ElimOnIdent of Names.lident
  3. | ElimOnAnonHyp of int
type !'a destruction_arg = clear_flag * 'a core_destruction_arg
val use_clear_hyp_by_default : unit -> bool
val intro_patterns : evars_flag -> 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 intros_patterns : evars_flag -> Tactypes.intro_patterns -> unit Proofview.tactic
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
type tactic_reduction = Reductionops.reduction_function
type e_tactic_reduction = Reductionops.e_reduction_function
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 : check:bool -> (tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
val e_reduct_in_concl : 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 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 unfold_constr : Names.GlobRef.t -> unit Proofview.tactic
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 -> EConstr.constr -> unit Proofview.tactic
val rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic
val revert : Names.Id.t list -> unit Proofview.tactic
val apply_type : typecheck:bool -> EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
val bring_hyps : EConstr.named_context -> unit Proofview.tactic
val apply : EConstr.constr -> unit Proofview.tactic
val eapply : EConstr.constr -> 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 : EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val cut_and_apply : EConstr.constr -> unit Proofview.tactic
type elim_scheme = {
  1. elimc : EConstr.constr Tactypes.with_bindings option;
  2. elimt : EConstr.types;
  3. indref : Names.GlobRef.t option;
  4. params : EConstr.rel_context;
  5. nparams : int;
  6. predicates : EConstr.rel_context;
  7. npredicates : int;
  8. branches : EConstr.rel_context;
  9. nbranches : int;
  10. args : EConstr.rel_context;
  11. nargs : int;
  12. indarg : EConstr.rel_declaration option;
  13. concl : EConstr.types;
  14. indarg_in_concl : bool;
  15. farg_in_concl : bool;
}
type eliminator = {
  1. elimindex : int option;
  2. elimbody : EConstr.constr Tactypes.with_bindings;
}
val general_elim_clause : evars_flag -> Unification.unify_flags -> Names.Id.t option -> Clenv.clausenv -> eliminator -> unit Proofview.tactic
val simplest_elim : EConstr.constr -> unit Proofview.tactic
val simplest_case : EConstr.constr -> unit Proofview.tactic
val case_type : EConstr.types -> unit Proofview.tactic
val elim_type : EConstr.types -> unit Proofview.tactic
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_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
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
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_as : bool -> Names.Id.t option -> Tactypes.intro_pattern option -> EConstr.constr -> 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 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 generalize : EConstr.constr list -> unit Proofview.tactic
val new_generalize_gen : ((Locus.occurrences * EConstr.constr) * Names.Name.t) list -> unit Proofview.tactic
val generalize_dep : ?with_let:bool -> EConstr.constr -> unit Proofview.tactic
val constr_eq : strict:bool -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Names.Id.t -> 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
module Simple : sig ... end
module New : sig ... end