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 * 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 -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.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 Exninfo.iexn
  2. | Next of 'a * Exninfo.iexn -> 'a tactic
val tclCASE : 'a tactic -> 'a case tactic
val tclBREAK : (Exninfo.iexn -> Exninfo.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 guard_no_unifiable : Names.Name.t list option tactic
val unshelve : Evar.t list -> proofview -> proofview
val filter_shelf : (Evar.t -> bool) -> 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