package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

val translate_vernac : 
  ?loc:Loc.t ->
  atts:Attributes.vernac_flags ->
  Vernacexpr.vernac_expr ->
  Vernacextend.typed_vernac

Vernac Translation into the Vernac DSL

val vernac_require : 
  Libnames.qualid option ->
  bool option ->
  Libnames.qualid list ->
  unit

Vernacular require command

val interp_redexp_hook : 
  (Environ.env ->
    Evd.evar_map ->
    Genredexpr.raw_red_expr ->
    Evd.evar_map * Redexpr.red_expr)
    Hook.t

Hook to dissappear when #8240 is fixed

Sourceval command_focus : unit Proof.focus_kind

Miscellaneous stuff

Sourceval allow_sprop_opt_name : string list