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 term : Constrexpr.constr_expr Entry.t
val ident : Names.Id.t Entry.t
val global : Libnames.qualid Entry.t
val universe_name : Constrexpr.sort_name_expr Entry.t
val sort : Constrexpr.sort_expr 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 cpattern : 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 one_open_binder : Constrexpr.kinded_cases_pattern_expr Entry.t
val one_closed_binder : Constrexpr.kinded_cases_pattern_expr 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 arg : (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) Entry.t
val type_cstr : Constrexpr.constr_expr Entry.t