package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val sig_it : 'a Evd.sigma -> 'a
val project : 'a Evd.sigma -> Evd.evar_map
val unpackage : 'a Evd.sigma -> Evd.evar_map ref * 'a
  • deprecated Do not use [evar_map ref]
val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma
  • deprecated Do not use [evar_map ref]
  • deprecated Do not use [evar_map ref]
val tclIDTAC : Proof_type.tactic
val tclIDTAC_MESSAGE : Pp.t -> Proof_type.tactic
val tclEVARUNIVCONTEXT : UState.t -> Proof_type.tactic
val tclPUSHEVARUNIVCONTEXT : UState.t -> Proof_type.tactic
val tclPUSHCONSTRAINTS : Univ.Constraint.t -> Proof_type.tactic
val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic
val tclTHENFIRSTn : Proof_type.tactic -> Proof_type.tactic array -> Proof_type.tactic
exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
val tclREPEAT_MAIN : Proof_type.tactic -> Proof_type.tactic
val tclFIRST : Proof_type.tactic list -> Proof_type.tactic
val tclSOLVE : Proof_type.tactic list -> Proof_type.tactic
val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
val tclFAIL : int -> Pp.t -> Proof_type.tactic
val tclFAIL_lazy : int -> Pp.t Lazy.t -> Proof_type.tactic
val tclDO : int -> Proof_type.tactic -> Proof_type.tactic
val tclIFTHENTRYELSEMUST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
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