package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type keyword_state
type te
type 'c pattern
type ty_pattern =
  1. | TPattern : 'a pattern -> ty_pattern

Type combinators to factor the module type between explicit state passing in Grammar and global state in Pcoq

type 'a with_gstate

Reader of grammar state

type 'a with_kwstate

Read keyword state

type 'a with_estate

Read entry state

type 'a mod_estate

Read/write entry state

module Parsable : sig ... end
module Entry : sig ... end
module Symbol : sig ... end
module Rule : sig ... end
module Rules : sig ... end
module Production : sig ... end
type 'a single_extend_statement = string option * Gramext.g_assoc option * 'a Production.t list
type 'a extend_statement =
  1. | Reuse of string option * 'a Production.t list
    (*

    Extend an existing level by its optional given name. If None, picks the topmost level.

    *)
  2. | Fresh of Gramext.position * 'a single_extend_statement list
    (*

    Create a level at the given position.

    *)
val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
OCaml

Innovation. Community. Security.