package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type tactic = Proofview.V82.tac
val sig_it : 'a Evd.sigma -> 'a
val project : 'a Evd.sigma -> Evd.evar_map
val refiner : check:bool -> Constr.t -> unit Proofview.tactic
val tclIDTAC : tactic
  • deprecated Use Tactical.New.tclIDTAC
val tclIDTAC_MESSAGE : Pp.t -> tactic
  • deprecated
val tclEVARS : Evd.evar_map -> tactic
  • deprecated Use Proofview.Unsafe.tclEVARS
val tclTHEN : tactic -> tactic -> tactic
  • deprecated Use Tactical.New.tclTHEN
val tclTHENLIST : tactic list -> tactic
  • deprecated Use Tactical.New.tclTHENLIST
val tclMAP : ('a -> tactic) -> 'a list -> tactic
  • deprecated Use Tactical.New.tclMAP
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
  • deprecated Use Tactical.New.tclTHEN_i
val tclTHENLAST : tactic -> tactic -> tactic
  • deprecated Use Tactical.New.tclTHENLAST
val tclTHENFIRST : tactic -> tactic -> tactic
  • deprecated Use Tactical.New.tclTHENFIRST
val tclTHENSV : tactic -> tactic array -> tactic
  • deprecated Use Tactical.New.tclTHENSV
val tclTHENS : tactic -> tactic list -> tactic
  • deprecated Use Tactical.New.tclTHENS
val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic
  • deprecated Use Tactical.New.tclTHENS3PARTS
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
  • deprecated Use Tactical.New.tclTHENSLASTn
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
  • deprecated Use Tactical.New.tclTHENSFIRSTn
exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
val tclORELSE0 : tactic -> tactic -> tactic
  • deprecated Use Tactical.New.tclORELSE0
val tclORELSE : tactic -> tactic -> tactic
  • deprecated Use Tactical.New.tclORELSE
val tclREPEAT : tactic -> tactic
  • deprecated Use Tactical.New.tclREPEAT
val tclFIRST : tactic list -> tactic
  • deprecated Use Tactical.New.tclFIRST
val tclTRY : tactic -> tactic
  • deprecated Use Tactical.New.tclTRY
val tclTHENTRY : tactic -> tactic -> tactic
  • deprecated Use Tactical.New.tclTHENTRY
val tclCOMPLETE : tactic -> tactic
  • deprecated Use Tactical.New.tclCOMPLETE
val tclAT_LEAST_ONCE : tactic -> tactic
  • deprecated Use Tactical.New.tclAT_LEAST_ONCE
val tclFAIL : int -> Pp.t -> tactic
  • deprecated Use Tactical.New.tclFAIL
val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic
  • deprecated Use Tactical.New.tclFAIL_lazy
val tclDO : int -> tactic -> tactic
  • deprecated Use Tactical.New.tclDO
val tclPROGRESS : tactic -> tactic
  • deprecated Use Tactical.New.tclPROGRESS
val tclSHOWHYPS : tactic -> tactic
  • deprecated Internal tactic. Do not use.
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