coq 8.13.1 · OCaml Package

val catch_failerror : Exninfo.iexn -> unit Proofview.tactic

val tclIDTAC : unit Proofview.tactic

val tclTHEN : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tactic

val tclZEROMSG : 
  ?info:Exninfo.info ->
  ?loc:Loc.t ->
  Pp.t ->
  'a Proofview.tactic

val tclOR : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclORD : 
  unit Proofview.tactic ->
  (unit -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclONCE : unit Proofview.tactic -> unit Proofview.tactic

val tclEXACTLY_ONCE : unit Proofview.tactic -> unit Proofview.tactic

val tclIFCATCH : 
  unit Proofview.tactic ->
  (unit -> unit Proofview.tactic) ->
  (unit -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclORELSE0 : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclORELSE : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclTHENS3PARTS : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENSLASTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENSFIRSTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclTHENFIRSTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENFIRST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclBINDFIRST : 
  'a Proofview.tactic ->
  ('a -> 'b Proofview.tactic) ->
  'b Proofview.tactic

val tclTHENLASTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENLAST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclBINDLAST : 
  'a Proofview.tactic ->
  ('a -> 'b Proofview.tactic) ->
  'b Proofview.tactic

val tclTHENS : 
  unit Proofview.tactic ->
  unit Proofview.tactic list ->
  unit Proofview.tactic

val tclTHENLIST : unit Proofview.tactic list -> unit Proofview.tactic

val tclMAP : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactic

val tclTRY : unit Proofview.tactic -> unit Proofview.tactic

val tclTRYb : unit Proofview.tactic -> bool list Proofview.tactic

val tclFIRST : unit Proofview.tactic list -> unit Proofview.tactic

val tclIFTHENELSE : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclIFTHENSVELSE : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclIFTHENTRYELSEMUST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclIFTHENFIRSTTRYELSEMUST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclDO : int -> unit Proofview.tactic -> unit Proofview.tactic

val tclREPEAT : unit Proofview.tactic -> unit Proofview.tactic

val tclREPEAT_MAIN : unit Proofview.tactic -> unit Proofview.tactic

val tclCOMPLETE : 'a Proofview.tactic -> 'a Proofview.tactic

val tclSOLVE : unit Proofview.tactic list -> unit Proofview.tactic

val tclPROGRESS : unit Proofview.tactic -> unit Proofview.tactic

val tclSELECT : Goal_select.t -> 'a Proofview.tactic -> 'a Proofview.tactic

val tclWITHHOLES : 
  bool ->
  'a Proofview.tactic ->
  Evd.evar_map ->
  'a Proofview.tactic

val tclDELAYEDWITHHOLES : 
  bool ->
  'a Tactypes.delayed_open ->
  ('a -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclMAPDELAYEDWITHHOLES : 
  bool ->
  'a Tactypes.delayed_open list ->
  ('a -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tactic

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

val nLastDecls : Proofview.Goal.t -> int -> EConstr.named_context

val ifOnHyp : 
  (Environ.env -> Evd.evar_map -> (Names.Id.t * EConstr.types) -> bool) ->
  (Names.Id.t -> unit Proofview.tactic) ->
  (Names.Id.t -> unit Proofview.tactic) ->
  Names.Id.t ->
  unit Proofview.tactic

val onNthHypId : 
  int ->
  (Names.Id.t -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onLastHypId : 
  (Names.Id.t -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onLastHyp : 
  (EConstr.constr -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onLastDecl : 
  (EConstr.named_declaration -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onNLastHypsId : 
  int ->
  (Names.Id.t list -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onNLastHyps : 
  int ->
  (EConstr.constr list -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onNLastDecls : 
  int ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onHyps : 
  (Proofview.Goal.t -> EConstr.named_context) ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

val afterHyp : 
  Names.Id.t ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tryAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic

val tryAllHypsAndConcl : 
  (Names.Id.t option -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onClause : 
  (Names.Id.t option -> unit Proofview.tactic) ->
  Locus.clause ->
  unit Proofview.tactic

val onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic

val onAllHypsAndConcl : 
  (Names.Id.t option -> unit Proofview.tactic) ->
  unit Proofview.tactic

val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family

val elimination_sort_of_hyp : Names.Id.t -> Proofview.Goal.t -> Sorts.family

val elimination_sort_of_clause : 
  Names.Id.t option ->
  Proofview.Goal.t ->
  Sorts.family

val pf_constr_of_global : Names.GlobRef.t -> EConstr.constr Proofview.tactic

val tclTYPEOFTHEN : 
  ?refresh:bool ->
  EConstr.constr ->
  (Evd.evar_map -> EConstr.types -> unit Proofview.tactic) ->
  unit Proofview.tactic

package coq