package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/ssreflect_plugin/Ssreflect_plugin/Ssripats/index.html

Module Ssreflect_plugin.SsripatsSource

Sourcetype 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
Sourceand ssriops = ssriop list
Sourceval tclCompileIPats : Ssrast.ssripats -> ssriops
Sourceval tclIPAT : ssriops -> unit Proofview.tactic
Sourceval tclIPATssr : Ssrast.ssripats -> unit Proofview.tactic
Sourceval ssrsmovetac : unit Proofview.tactic
Sourceval ssrselimtoptac : unit Proofview.tactic
Sourceval ssrscasetoptac : unit Proofview.tactic
Sourceval ssrabstract : Ssrast.ssrdgens -> unit Proofview.tactic
Sourcemodule Internal : sig ... end