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