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