package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val e_assumption : unit Proofview.tactic
val registered_e_assumption : unit Proofview.tactic
val e_give_exact : ?flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic
val gen_eauto : ?debug:Hints.debug -> (bool * int) -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
val eauto_with_bases : ?debug:Hints.debug -> (bool * int) -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> unit Proofview.tactic
val autounfold : Hints.hint_db_name list -> Locus.clause -> unit Proofview.tactic
val autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tactic
val autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic
val make_depth : int option -> int
val make_dimension : int option -> int option -> bool * int
OCaml

Innovation. Community. Security.