package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val binder_constr : Constrexpr.constr_expr Entry.t
  • deprecated Deprecated in 8.13; use 'term' instead
val ident : Names.Id.t Entry.t
val universe_level : Constrexpr.univ_level_expr Entry.t
val sort_family : Sorts.family Entry.t
val constr_pattern : Constrexpr.constr_expr Entry.t
val lconstr_pattern : Constrexpr.constr_expr Entry.t
  • deprecated Deprecated in 8.13; use 'cpattern' instead
val closed_binder : Constrexpr.local_binder_expr list Entry.t
val open_binders : Constrexpr.local_binder_expr list Entry.t
val typeclass_constraint : (Names.lname * bool * Constrexpr.constr_expr) Entry.t
val record_declaration : Constrexpr.constr_expr Entry.t
  • deprecated Deprecated in 8.13; use 'arg' instead