package coq

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Number_string_notation_plugin.NumberSource

* Number notation

Sourcetype number_string_via = Libnames.qualid * (bool * Libnames.qualid * Libnames.qualid) list
Sourcetype number_option =
  1. | After of Notation.numnot_option
  2. | Via of number_string_via
Sourceval locate_global_inductive : bool -> Libnames.qualid -> Names.inductive * Names.GlobRef.t option list

These are also used in string notations

Sourceval elaborate_to_post_params : Environ.env -> Evd.evar_map -> Names.inductive -> Names.GlobRef.t option list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
OCaml

Innovation. Community. Security.