Hi, coq/coq#17084 intends to make uniform the interpretation of references depending on whether the reference is interpreted at toplevel or within an Ltac definitions or tactic notations. In particular, it now always insert maximal implicit arguments, like already the case at toplevel, even when in Ltac definition or tactic notation.
As a consequence, in LeaderLogsTermSanityProof.v, an eq_refl must be changed to @eq_refl to preserve the original behavior, in anticipation of coq/coq#17084.
This is backwards compatible and can be merged as soon as now.
Hi, coq/coq#17084 intends to make uniform the interpretation of references depending on whether the reference is interpreted at toplevel or within an Ltac definitions or tactic notations. In particular, it now always insert maximal implicit arguments, like already the case at toplevel, even when in Ltac definition or tactic notation.
As a consequence, in
LeaderLogsTermSanityProof.v, aneq_reflmust be changed to@eq_reflto preserve the original behavior, in anticipation of coq/coq#17084.This is backwards compatible and can be merged as soon as now.