package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a entry = 'a Grammar.GMake(CLexer).Entry.e
type side =
  1. | Left
  2. | Right
type gram_assoc =
  1. | NonA
  2. | RightA
  3. | LeftA
type gram_position =
  1. | First
  2. | Last
  3. | Before of string
  4. | After of string
  5. | Level of string
type production_position =
  1. | BorderProd of side * gram_assoc option
  2. | InternalProd
type production_level =
  1. | NextLevel
  2. | NumLevel of int
type !'a constr_entry_key_gen =
  1. | ETIdent
  2. | ETGlobal
  3. | ETBigint
  4. | ETBinder of bool
  5. | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
  6. | ETPattern of bool * int option
type constr_entry_key = (production_level * production_position) constr_entry_key_gen
type simple_constr_prod_entry_key = production_level option constr_entry_key_gen
type binder_entry_kind =
  1. | ETBinderOpen
  2. | ETBinderClosed of Tok.t list
type binder_target =
  1. | ForBinder
  2. | ForTerm
type constr_prod_entry_key =
  1. | ETProdName
  2. | ETProdReference
  3. | ETProdBigint
  4. | ETProdConstr of Constrexpr.notation_entry * production_level * production_position
  5. | ETProdPattern of int
  6. | ETProdConstrList of production_level * production_position * Tok.t list
  7. | ETProdBinderList of binder_entry_kind
type !'a user_symbol =
  1. | Ulist1 of 'a user_symbol
  2. | Ulist1sep of 'a user_symbol * string
  3. | Ulist0 of 'a user_symbol
  4. | Ulist0sep of 'a user_symbol * string
  5. | Uopt of 'a user_symbol
  6. | Uentry of 'a
  7. | Uentryl of 'a * int
type (!'a6, !'b6, !'c6) ty_user_symbol =
  1. | TUlist1 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
  2. | TUlist1sep : ('a0, 'b0, 'c0) ty_user_symbol * string -> ('a0 list, 'b0 list, 'c0 list) ty_user_symbol
  3. | TUlist0 : ('a1, 'b1, 'c1) ty_user_symbol -> ('a1 list, 'b1 list, 'c1 list) ty_user_symbol
  4. | TUlist0sep : ('a2, 'b2, 'c2) ty_user_symbol * string -> ('a2 list, 'b2 list, 'c2 list) ty_user_symbol
  5. | TUopt : ('a3, 'b3, 'c3) ty_user_symbol -> ('a3 option, 'b3 option, 'c3 option) ty_user_symbol
  6. | TUentry : ('a4, 'b4, 'c4) Genarg.ArgT.tag -> ('a4, 'b4, 'c4) ty_user_symbol
  7. | TUentryl : ('a5, 'b5, 'c5) Genarg.ArgT.tag * int -> ('a5, 'b5, 'c5) ty_user_symbol
type (!'self10, !'a7) symbol =
  1. | Atoken : Tok.t -> ('self, string) symbol
  2. | Alist1 : ('self0, 'a) symbol -> ('self0, 'a list) symbol
  3. | Alist1sep : ('self1, 'a0) symbol * ('self1, 'b) symbol -> ('self1, 'a0 list) symbol
  4. | Alist0 : ('self2, 'a1) symbol -> ('self2, 'a1 list) symbol
  5. | Alist0sep : ('self3, 'a2) symbol * ('self3, 'c) symbol -> ('self3, 'a2 list) symbol
  6. | Aopt : ('self4, 'a3) symbol -> ('self4, 'a3 option) symbol
  7. | Aself : ('self5, 'self5) symbol
  8. | Anext : ('self6, 'self6) symbol
  9. | Aentry : 'a4 entry -> ('self7, 'a4) symbol
  10. | Aentryl : 'a5 entry * string -> ('self8, 'a5) symbol
  11. | Arules : 'a6 rules list -> ('self9, 'a6) symbol
and (!'self1, !_, !'r1) rule =
  1. | Stop : ('self, 'r, 'r) rule
  2. | Next : ('self0, 'a, 'r0) rule * ('self0, 'b) symbol -> ('self0, 'b -> 'a, 'r0) rule
and (!'a, !'r) norec_rule = {
  1. norec_rule : 's. ('s, 'a, 'r) rule;
}
and !'a0 rules =
  1. | Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
type !'a0 production_rule =
  1. | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
type !'a single_extend_statement = string option * gram_assoc option * 'a production_rule list
type !'a extend_statement = gram_position option * 'a single_extend_statement list
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