package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Local reimplementations of tactics variants from Coq

val intros_patterns : Tac2types.evars_flag -> Tac2types.intro_pattern 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 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 lazy_ : Names.GlobRef.t Genredexpr.glob_red_flag -> Tac2types.clause -> 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 contradiction : Tac2types.constr_with_bindings option -> unit Proofview.tactic