package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.parsing/Extend/index.html

Module ExtendSource

Entry keys for constr notations

Sourcetype production_position =
  1. | BorderProd of Constrexpr.side * Gramlib.Gramext.g_assoc option
  2. | InternalProd
Sourcetype production_level =
  1. | NextLevel
  2. | NumLevel of int
  3. | DefaultLevel
    (*

    Interpreted differently at the border or inside a rule

    *)
Sourceval production_level_eq : production_level -> production_level -> bool

User-level types used to tell how to parse or interpret of the non-terminal

Sourcetype 'a constr_entry_key_gen =
  1. | ETIdent
  2. | ETName
  3. | ETGlobal
  4. | ETBigint
  5. | ETBinder of bool
  6. | ETConstr of Constrexpr.notation_entry * Notation_term.notation_binder_kind option * 'a
  7. | ETPattern of bool * int option

Entries level (left-hand side of grammar rules)

Sourcetype constr_entry_key = (production_level * production_position) constr_entry_key_gen
Sourceval constr_entry_key_eq : constr_entry_key -> constr_entry_key -> bool

Entries used in productions, vernac side (e.g. "x bigint" or "x ident")

Sourcetype simple_constr_prod_entry_key = production_level constr_entry_key_gen

Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals

Sourcetype binder_target =
  1. | ForBinder
  2. | ForTerm
Sourcetype binder_entry_kind =
  1. | ETBinderOpen
  2. | ETBinderClosed of constr_prod_entry_key option * (bool * string) list
Sourceand constr_prod_entry_key =
  1. | ETProdIdent
  2. | ETProdName
  3. | ETProdGlobal
  4. | ETProdBigint
  5. | ETProdOneBinder of bool
  6. | ETProdConstr of Constrexpr.notation_entry * production_level * production_position
  7. | ETProdPattern of int
  8. | ETProdConstrList of Constrexpr.notation_entry * production_level * production_position * (bool * string) list
  9. | ETProdBinderList of binder_entry_kind
AST for user-provided entries
Sourcetype '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
Sourcetype ('a, 'b, 'c) ty_user_symbol =
  1. | TUlist1 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
  2. | TUlist1sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol
  3. | TUlist0 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
  4. | TUlist0sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol
  5. | TUopt : ('a, 'b, 'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
  6. | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a, 'b, 'c) ty_user_symbol
  7. | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a, 'b, 'c) ty_user_symbol