Module `G_constr`

val ldots_var : Names.Id.t
val constr_kw : string list
val mk_cast : (Constrexpr.constr_expr * ('a * Constrexpr.constr_expr option)) -> Constrexpr.constr_expr
val binder_of_name : Glob_term.binding_kind -> Names.Name.t CAst.t -> Constrexpr.local_binder_expr
val binders_of_names : Names.Name.t CAst.t list -> Constrexpr.local_binder_expr list
val mk_fixb : (Names.lident * Constrexpr.local_binder_expr list * Constrexpr.recursion_order_expr option * Constrexpr.constr_expr * ('a * Constrexpr.constr_expr option)) -> Constrexpr.fix_expr
val mk_cofixb : (Names.lident * Constrexpr.local_binder_expr list * 'a CAst.t option * Constrexpr.constr_expr * ('b * Constrexpr.constr_expr option)) -> Constrexpr.cofix_expr
val mk_fix : (Loc.t * bool * Names.lident * (Names.lident * Constrexpr.local_binder_expr list * Constrexpr.recursion_order_expr option * Constrexpr.constr_expr * ('a * Constrexpr.constr_expr option)) list) -> Constrexpr.constr_expr_r CAst.t
val mk_single_fix : (Loc.t * bool * (Names.lident * Constrexpr.local_binder_expr list * Constrexpr.recursion_order_expr option * Constrexpr.constr_expr * ('a * Constrexpr.constr_expr option))) -> Constrexpr.constr_expr_r CAst.t
val err : unit -> 'a
val lpar_id_coloneq : Names.Id.t Pcoq.Entry.t
val impl_ident_head : Names.Id.t Pcoq.Entry.t
val name_colon : Names.name Pcoq.Entry.t
val aliasvar : Constrexpr.cases_pattern_expr_r CAst.t -> Names.lname option