Module `Pcoq.Constr`

val constr : Constrexpr.constr_expr Entry.t
val constr_eoi : Constrexpr.constr_expr Entry.t
val lconstr : Constrexpr.constr_expr Entry.t
val binder_constr : Constrexpr.constr_expr Entry.t
val operconstr : Constrexpr.constr_expr Entry.t
val ident : Names.Id.t Entry.t
val global : Libnames.qualid Entry.t
val universe_name : Glob_term.glob_sort_name Entry.t
val universe_level : Glob_term.glob_level Entry.t
val sort : Glob_term.glob_sort Entry.t
val sort_family : Sorts.family Entry.t
val pattern : Constrexpr.cases_pattern_expr Entry.t
val constr_pattern : Constrexpr.constr_expr Entry.t
val lconstr_pattern : Constrexpr.constr_expr Entry.t
val closed_binder : Constrexpr.local_binder_expr list Entry.t
val binder : Constrexpr.local_binder_expr list Entry.t
val binders : Constrexpr.local_binder_expr list Entry.t
val open_binders : Constrexpr.local_binder_expr list Entry.t
val binders_fixannot : (Constrexpr.local_binder_expr list * Constrexpr.recursion_order_expr option) Entry.t
val typeclass_constraint : (Names.lname * bool * Constrexpr.constr_expr) Entry.t
val record_declaration : Constrexpr.constr_expr Entry.t
val appl_arg : (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) Entry.t