package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type proofview
val proofview : proofview -> Evar.t list * Evd.evar_map
type entry
val compact : entry -> proofview -> entry * proofview
val dependent_init : telescope -> entry * proofview
val finished : proofview -> bool
val return : proofview -> Evd.evar_map
val partial_proof : entry -> proofview -> EConstr.constr list
val initial_goals : entry -> (EConstr.constr * EConstr.types) list
type focus_context
val focus_context : focus_context -> Evar.t list * Evar.t list
val focus : int -> int -> proofview -> proofview * focus_context
val unfocus : focus_context -> proofview -> proofview
type +'a tactic
val apply : name:Names.Id.t -> poly:bool -> Environ.env -> 'a tactic -> proofview -> 'a * proofview * (bool * Evar.t list * Evar.t list) * Proofview_monad.Info.tree
val tclUNIT : 'a -> 'a tactic
val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
val tclIGNORE : 'a tactic -> unit tactic
module Monad : sig ... end
val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
val tclOR : 'a tactic -> (Util.iexn -> 'a tactic) -> 'a tactic
val tclORELSE : 'a tactic -> (Util.iexn -> 'a tactic) -> 'a tactic
val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Util.iexn -> 'b tactic) -> 'b tactic
val tclONCE : 'a tactic -> 'a tactic
exception MoreThanOneSuccess
val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
type !'a case =
  1. | Fail of Util.iexn
  2. | Next of 'a * Util.iexn -> 'a tactic
val tclCASE : 'a tactic -> 'a case tactic
val tclBREAK : (Util.iexn -> Util.iexn option) -> 'a tactic -> 'a tactic
exception NoSuchGoals of int
val tclFOCUS : ?nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic
val tclFOCUSLIST : ?nosuchgoal:'a tactic -> (int * int) list -> 'a tactic -> 'a tactic
val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic
val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic
exception SizeMismatch of int * int
val tclDISPATCH : unit tactic list -> unit tactic
val tclDISPATCHL : 'a tactic list -> 'a list tactic
val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
val tclINDEPENDENT : unit tactic -> unit tactic
val tclINDEPENDENTL : 'a tactic -> 'a list tactic
val shelve : unit tactic
val shelve_goals : Evar.t list -> unit tactic
val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool
val shelve_unifiable : unit tactic
val shelve_unifiable_informative : Evar.t list tactic
val guard_no_unifiable : Names.Name.t list option tactic
val unshelve : Evar.t list -> proofview -> proofview
val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool
val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic
val cycle : int -> unit tactic
val swap : int -> int -> unit tactic
val revgoals : unit tactic
val numgoals : int tactic
val tclEVARMAP : Evd.evar_map tactic
val tclENV : Environ.env tactic
val tclEFFECTS : Evd.side_effects -> unit tactic
val mark_as_unsafe : unit tactic
val give_up : unit tactic
val tclPROGRESS : 'a tactic -> 'a tactic
module Progress : sig ... end
val tclCHECKINTERRUPT : unit tactic
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
val tclTIME : string option -> 'a tactic -> 'a tactic
val tclProofInfo : (Names.Id.t * bool) tactic
  • deprecated internal, don't use
module Unsafe : sig ... end
module UnsafeRepr : sig ... end
module Goal : sig ... end
module Trace : sig ... end
module NonLogical : sig ... end
val tclLIFT : 'a NonLogical.t -> 'a tactic
module V82 : sig ... end
module Notations : sig ... end
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