package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type te = Tok.t
type parsable
val parsable : char Stream.t -> parsable
val tokens : string -> (string * int) list
val glexer : te Plexing.lexer
val set_algorithm : Grammar.parse_algorithm -> unit
module Entry : sig ... end
type ('self, 'a) ty_symbol
type ('self, 'f, 'r) ty_rule
type 'a ty_production
val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol
val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
val s_list0sep : ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> ('self, 'a list) ty_symbol
val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
val s_list1sep : ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> ('self, 'a list) ty_symbol
val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
val s_flag : ('self, 'a) ty_symbol -> ('self, bool) ty_symbol
val s_self : ('self, 'self) ty_symbol
val s_next : ('self, 'self) ty_symbol
val s_token : Plexing.pattern -> ('self, string) ty_symbol
val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol
val s_vala : string list -> ('self, 'a) ty_symbol -> ('self, 'a Ploc.vala) ty_symbol
val r_stop : ('self, 'r, 'r) ty_rule
val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule
val r_cut : ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule
val production : (('a, 'f, Ploc.t -> 'a) ty_rule * 'f) -> 'a ty_production
module Unsafe : sig ... end
val extend : 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * (te Gramext.g_symbol list * Gramext.g_action) list) list -> unit
val safe_extend : 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> unit
val delete_rule : 'a Entry.e -> te Gramext.g_symbol list -> unit
val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit
type 'a entry = 'a Entry.e
  • deprecated Use [Pcoq.Entry.t]
val entry_create : string -> 'a entry
  • deprecated Use [Pcoq.Entry.create]
val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit