package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.tactics/Eauto/index.html

Module EautoSource

Sourceval e_assumption : unit Proofview.tactic
Sourceval registered_e_assumption : unit Proofview.tactic
Sourceval gen_eauto : ?debug:Hints.debug -> (bool * int) -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
Sourceval eauto_with_bases : ?debug:Hints.debug -> (bool * int) -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> unit Proofview.tactic
Sourceval autounfold : Hints.hint_db_name list -> Locus.clause -> unit Proofview.tactic
Sourceval autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tactic
Sourceval autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic
Sourceval make_depth : int option -> int
Sourceval make_dimension : int option -> int option -> bool * int
OCaml

Innovation. Community. Security.