ComRewriteRuleval do_symbols : poly:PolyFlags.t -> unfold_fix:bool ->
(Vernacexpr.coercion_flag * ((Names.lident * Constrexpr.universe_decl_expr option) list * Constrexpr.constr_expr)) list -> unitval do_rules : ?collapse_sort_variables:bool -> Names.Id.t -> (Constrexpr.universe_decl_expr option * Constrexpr.constr_expr * Constrexpr.constr_expr) list -> unit