Closed herbelin closed 3 months ago
This concerns fixpoint_expr, cofixpoint_expr, recursion_order_expr, etc., in constrexpr.mli or vernacexpr.mli.
fixpoint_expr
cofixpoint_expr
recursion_order_expr
constrexpr.mli
vernacexpr.mli
To be merged synchronously with coq/coq#19107.
Please merge now
ping @ejgallego
Will merge ASAP, you are welcome folks to merge yourselves too if I'm in holidays like last week.
This concerns
fixpoint_expr
,cofixpoint_expr
,recursion_order_expr
, etc., inconstrexpr.mli
orvernacexpr.mli
.To be merged synchronously with coq/coq#19107.