package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val add_token_obj : string -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit
val add_delimiters : Notation_term.scope_name -> string -> unit
val remove_delimiters : Notation_term.scope_name -> unit
val add_class_scope : Notation_term.scope_name -> Notation.scope_class list -> unit
val add_notation_interpretation : (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) -> unit
val set_notation_for_interpretation : Constrintern.internalization_env -> (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) -> unit
val add_syntax_extension : Vernacexpr.locality_flag -> (Vernacexpr.lstring * Vernacexpr.syntax_modifier list) -> unit
val add_syntactic_definition : Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> bool -> Flags.compat_version option -> unit
val pr_grammar : string -> Pp.std_ppcmds
type any_entry =
  1. | AnyEntry : 'a Pcoq.Gram.entry -> any_entry
val register_grammar : string -> any_entry list -> unit
val check_infix_modifiers : Vernacexpr.syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
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