package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ssrwkind =
  1. | RWred of Ssrast.ssrsimpl
  2. | RWdef
  3. | RWeq
type ssrrule = ssrwkind * Ssrast.ssrterm
val dir_org : Ssrast.ssrdir -> int
val notimes : int
val nomult : Ssrast.ssrmult
val nodocc : Ssrast.ssrdocc
val noclr : Ssrast.ssrdocc
val simpltac : Ssrast.ssrsimpl -> unit Proofview.tactic
val newssrcongrtac : (int * Ssrast.ssrterm) -> Ltac_plugin.Tacinterp.interp_sign -> unit Proofview.tactic
val norwmult : Ssrast.ssrdir * Ssrast.ssrmult
val ssr_is_setoid : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool
val ssrrewritetac : ?under:bool -> ?map_redex: (Environ.env -> Evd.evar_map -> before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) -> Ltac_plugin.Tacinterp.interp_sign -> ssrrwarg list -> unit Proofview.tactic
val ipat_rewrite : Ssrast.ssrocc -> Ssrast.ssrdir -> EConstr.t -> unit Proofview.tactic