package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type syndef_interpretation = (Names.Id.t * Notation_term.subscopes) list * Notation_term.notation_constr
val declare_syntactic_definition : bool -> Names.Id.t -> Flags.compat_version option -> syndef_interpretation -> unit
val search_syntactic_definition : ?loc:Loc.t -> Names.KerName.t -> syndef_interpretation
val search_filtered_syntactic_definition : ?loc:Loc.t -> (syndef_interpretation -> 'a option) -> Names.KerName.t -> 'a option