Adapt to coq/coq#18273 (Ltac2 supports head reduction)#1725

Merged

JasonGross merged 3 commits intomit-plv:masterfrom SkySkimmer:ltac2-head-red

Nov 14, 2023

+3-5

Commits on Nov 13, 2023

Adapt to coq/coq#18273 (Ltac2 supports head reduction)

SkySkimmer
authored and
JasonGross
committed
Update IdentifierParameters.v according to review comment

SkySkimmer
authored and
JasonGross
committed
Parenthesize red_flags
JasonGross
committed