package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.2.tar.gz

sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

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

Module `Eauto`Source

Sourceval e_assumption : unit Proofview.tactic

Sourceval registered_e_assumption : unit Proofview.tactic

Source

val e_give_exact : 
  ?flags:Unification.unify_flags ->
  EConstr.constr ->
  unit Proofview.tactic

Source

val gen_eauto : 
  ?debug:Hints.debug ->
  (bool * int) ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db_name list option ->
  unit Proofview.tactic

Source

val eauto_with_bases : 
  ?debug:Hints.debug ->
  (bool * int) ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db list ->
  unit Proofview.tactic

Source

val autounfold : 
  Hints.hint_db_name list ->
  Locus.clause ->
  unit Proofview.tactic

Source

val autounfold_tac : 
  Hints.hint_db_name list option ->
  Locus.clause ->
  unit Proofview.tactic

Source

val 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

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module EautoSource

Module `Eauto`Source