Closing sections or modules prints backtracking and redoing byextend on command in 8.17.0

[Janno]

Description of the problem

This message can be generated easily by

Succeed From Ltac2 Require Import Ltac2.

but it also comes up when closing sections or modules that contain Import commands. We have not managed to minimize this but it seems to depend on the order of Import commands. Maybe it is because the imported modules have overlapping dependencies and when Coq notices this it undoes the repeated import of those dependencies?

The printed message was introduced by @SkySkimmer in #17069. (It doesn't have line number or file name information so it's actually a bit tricky to track down where it is emitted.)

Coq Version

8.17.0

[SkySkimmer]

That's a debug message that I forgot to cleanup. I guess we should do a 8.17.1 with it removed since there is no way to turn it off.