coq 8.7.2 · OCaml Package

type proofview

val proofview : proofview -> Evd.evar list * Evd.evar_map

type entry

val compact : entry -> proofview -> entry * proofview

val init : 
  Evd.evar_map ->
  (Environ.env * EConstr.types) list ->
  entry * proofview

type telescope =

| TNil of Evd.evar_map
| TCons of Environ.env * Evd.evar_map * EConstr.types * Evd.evar_map -> EConstr.constr -> telescope

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 -> Evd.evar list * Evd.evar list

val focus : int -> int -> proofview -> proofview * focus_context

val unfocus : focus_context -> proofview -> proofview

type +'a tactic

val apply : 
  Environ.env ->
  'a tactic ->
  proofview ->
  'a
  * proofview
  * (bool * Evd.evar list * Evd.evar 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 =

| Fail of Util.iexn
| 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 set_nosuchgoals_hook : (int -> Pp.std_ppcmds) -> unit

val tclFOCUS : int -> int -> 'a tactic -> 'a tactic

val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic

val tclFOCUSID : 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 : Evd.evar list -> unit tactic

val unifiable : Evd.evar_map -> Evd.evar -> Evd.evar list -> bool

val shelve_unifiable : unit tactic

val guard_no_unifiable : Names.Name.t list option tactic

val unshelve : Evd.evar list -> proofview -> proofview

val depends_on : Evd.evar_map -> Evd.evar -> Evd.evar -> bool

val with_shelf : 'a tactic -> (Evd.evar 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 : Safe_typing.private_constants -> unit tactic

val mark_as_unsafe : unit tactic

val give_up : unit tactic

val tclPROGRESS : 'a tactic -> 'a tactic

val tclCHECKINTERRUPT : unit tactic

exception Timeout

val tclTIMEOUT : int -> 'a tactic -> 'a tactic

val tclTIME : string option -> 'a tactic -> 'a tactic

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

package coq