package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type side =
  1. | Left
  2. | Right
type production_position =
  1. | BorderProd of side * Gramlib.Gramext.g_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 simple_constr_prod_entry_key = production_level option constr_entry_key_gen
type binder_entry_kind =
  1. | ETBinderOpen
  2. | ETBinderClosed of string Tok.p 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 Constrexpr.notation_entry * production_level * production_position * string Tok.p 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, !'trec4, !'a7) symbol =
  1. | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
  2. | Alist1 : ('self0, 'trec, 'a) symbol -> ('self0, 'trec, 'a list) symbol
  3. | Alist1sep : ('self1, 'trec0, 'a0) symbol * ('self1, norec, 'b) symbol -> ('self1, 'trec0, 'a0 list) symbol
  4. | Alist0 : ('self2, 'trec1, 'a1) symbol -> ('self2, 'trec1, 'a1 list) symbol
  5. | Alist0sep : ('self3, 'trec2, 'a2) symbol * ('self3, norec, 'd) symbol -> ('self3, 'trec2, 'a2 list) symbol
  6. | Aopt : ('self4, 'trec3, 'a3) symbol -> ('self4, 'trec3, 'a3 option) symbol
  7. | Aself : ('self5, mayrec, 'self5) symbol
  8. | Anext : ('self6, mayrec, 'self6) symbol
  9. | Aentry : 'a4 entry -> ('self7, norec, 'a4) symbol
  10. | Aentryl : 'a5 entry * string -> ('self8, norec, 'a5) symbol
  11. | Arules : 'a6 rules list -> ('self9, norec, 'a6) symbol
and (!'self2, !'trec, !_, !'r2) rule =
  1. | Stop : ('self, norec, 'r, 'r) rule
  2. | Next : ('self0, 'c, 'a, 'r0) rule * ('self0, 'd, 'b) symbol -> ('self0, mayrec, 'b -> 'a, 'r0) rule
  3. | NextNoRec : ('self1, norec, 'a0, 'r1) rule * ('self1, norec, 'b0) symbol -> ('self1, norec, 'b0 -> 'a0, 'r1) rule
and !'a0 rules =
  1. | Rules : ('b, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules
type !'a0 production_rule =
  1. | Rule : ('a, 'b, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
OCaml

Innovation. Community. Security.