package coq

  1. Overview
  2. Docs
package coq
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 prolog_tac : Tactypes.delayed_open_constr list -> int -> 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_dimension : int option -> int option -> bool * int
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct