package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ssriop =
  1. | IOpId of Names.Id.t
  2. | IOpDrop
  3. | IOpTemporay
  4. | IOpInaccessible of string option
  5. | IOpInaccessibleAll
  6. | IOpAbstractVars of Names.Id.t list
  7. | IOpFastNondep
  8. | IOpInj of ssriops list
  9. | IOpDispatchBlock of Ssrast.id_block
  10. | IOpDispatchBranches of ssriops list
  11. | IOpCaseBlock of Ssrast.id_block
  12. | IOpCaseBranches of ssriops list
  13. | IOpRewrite of Ssrast.ssrocc * Ssrast.ssrdir
  14. | IOpView of Ssrast.ssrclear option * Ssrast.ssrview
  15. | IOpClear of Ssrast.ssrclear * Ssrast.ssrhyp option
  16. | IOpSimpl of Ssrast.ssrsimpl
  17. | IOpEqGen of unit Proofview.tactic
  18. | IOpNoop
and ssriops = ssriop list
val tclCompileIPats : Ssrast.ssripats -> ssriops
val tclIPAT : ssriops -> unit Proofview.tactic
val tclIPATssr : Ssrast.ssripats -> unit Proofview.tactic
val ssrsmovetac : unit Proofview.tactic
val ssrselimtoptac : unit Proofview.tactic
val ssrscasetoptac : unit Proofview.tactic
val ssrabstract : Ssrast.ssrdgens -> unit Proofview.tactic
module Internal : sig ... end
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