package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/ltac2_plugin/Ltac2_plugin/Tac2tactics/index.html
Module Ltac2_plugin.Tac2tacticsSource
Local reimplementations of tactics variants from Coq
Source
val intros_patterns :
Tac2types.evars_flag ->
Tac2types.intro_pattern list ->
unit Proofview.tacticSource
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.tacticSource
val induction_destruct :
Tac2expr.rec_flag ->
Tac2types.evars_flag ->
Tac2types.induction_clause list ->
Tac2types.constr_with_bindings option ->
unit Proofview.tacticSource
val elim :
Tac2types.evars_flag ->
Tac2types.constr_with_bindings ->
Tac2types.constr_with_bindings option ->
unit Proofview.tacticSource
val general_case_analysis :
Tac2types.evars_flag ->
Tac2types.constr_with_bindings ->
unit Proofview.tacticSource
val generalize :
(EConstr.constr * Tac2types.occurrences * Names.Name.t) list ->
unit Proofview.tacticSource
val constructor_tac :
Tac2types.evars_flag ->
int option ->
int ->
Tac2types.bindings ->
unit Proofview.tacticSource
val specialize :
Tac2types.constr_with_bindings ->
Tac2types.intro_pattern option ->
unit Proofview.tacticSource
val change :
Pattern.constr_pattern option ->
(EConstr.constr array, EConstr.constr) Tac2ffi.fun1 ->
Tac2types.clause ->
unit Proofview.tacticSource
val rewrite :
Tac2types.evars_flag ->
Tac2types.rewriting list ->
Tac2types.clause ->
unit Tac2types.thunk option ->
unit Proofview.tacticSource
val forward :
bool ->
unit Proofview.tactic option option ->
Tac2types.intro_pattern option ->
EConstr.constr ->
unit Proofview.tacticSource
val letin_pat_tac :
Tac2types.evars_flag ->
(bool * Tac2types.intro_pattern_naming) option ->
Names.Name.t ->
(Evd.evar_map * EConstr.constr) ->
Tac2types.clause ->
unit Proofview.tacticSource
val simpl :
Names.GlobRef.t Genredexpr.glob_red_flag ->
(Pattern.constr_pattern * Tac2types.occurrences) option ->
Tac2types.clause ->
unit Proofview.tacticSource
val cbv :
Names.GlobRef.t Genredexpr.glob_red_flag ->
Tac2types.clause ->
unit Proofview.tacticSource
val cbn :
Names.GlobRef.t Genredexpr.glob_red_flag ->
Tac2types.clause ->
unit Proofview.tacticSource
val lazy_ :
Names.GlobRef.t Genredexpr.glob_red_flag ->
Tac2types.clause ->
unit Proofview.tacticSource
val unfold :
(Names.GlobRef.t * Tac2types.occurrences) list ->
Tac2types.clause ->
unit Proofview.tacticSource
val pattern :
(EConstr.constr * Tac2types.occurrences) list ->
Tac2types.clause ->
unit Proofview.tacticSource
val vm :
(Pattern.constr_pattern * Tac2types.occurrences) option ->
Tac2types.clause ->
unit Proofview.tacticSource
val native :
(Pattern.constr_pattern * Tac2types.occurrences) option ->
Tac2types.clause ->
unit Proofview.tacticSource
val eval_simpl :
Names.GlobRef.t Genredexpr.glob_red_flag ->
(Pattern.constr_pattern * Tac2types.occurrences) option ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_cbv :
Names.GlobRef.t Genredexpr.glob_red_flag ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_cbn :
Names.GlobRef.t Genredexpr.glob_red_flag ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_lazy :
Names.GlobRef.t Genredexpr.glob_red_flag ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_unfold :
(Names.GlobRef.t * Tac2types.occurrences) list ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_pattern :
(EConstr.t * Tac2types.occurrences) list ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_vm :
(Pattern.constr_pattern * Tac2types.occurrences) option ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val eval_native :
(Pattern.constr_pattern * Tac2types.occurrences) option ->
EConstr.constr ->
EConstr.constr Proofview.tacticSource
val discriminate :
Tac2types.evars_flag ->
Tac2types.destruction_arg option ->
unit Proofview.tacticSource
val injection :
Tac2types.evars_flag ->
Tac2types.intro_pattern list option ->
Tac2types.destruction_arg option ->
unit Proofview.tacticSource
val autorewrite :
all:bool ->
unit Tac2types.thunk option ->
Names.Id.t list ->
Tac2types.clause ->
unit Proofview.tacticSource
val trivial :
Hints.debug ->
EConstr.constr Tac2types.thunk list ->
Names.Id.t list option ->
unit Proofview.tacticSource
val auto :
Hints.debug ->
int option ->
EConstr.constr Tac2types.thunk list ->
Names.Id.t list option ->
unit Proofview.tacticSource
val new_auto :
Hints.debug ->
int option ->
EConstr.constr Tac2types.thunk list ->
Names.Id.t list option ->
unit Proofview.tacticSource
val eauto :
Hints.debug ->
int option ->
int option ->
EConstr.constr Tac2types.thunk list ->
Names.Id.t list option ->
unit Proofview.tacticSource
val typeclasses_eauto :
Class_tactics.search_strategy option ->
int option ->
Names.Id.t list option ->
unit Proofview.tacticSource
val inversion :
Inv.inversion_kind ->
Tac2types.destruction_arg ->
Tac2types.intro_pattern option ->
Names.Id.t list option ->
unit Proofview.tactic