package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
val tactic : ?nf_evars:bool -> tac -> unit tactic
val nf_evar_goals : unit tactic
val has_unresolved_evar : proofview -> bool
val grab : proofview -> proofview
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
val top_evars : entry -> proofview -> Evar.t list
val of_tactic : 'a tactic -> tac
val put_status : bool -> unit tactic
val catchable_exception : exn -> bool
val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
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