Set Warnings doesn't seem STM-aware. In VsCoq, undoing it by stepping back doesn't undo its side effects correctly. And this snippet gives different results depending on how you step through it:
Require Import ssreflect. Set Warnings "-ssr-search-moved". Search "++".
Going step-by-step works correctly. When jumping to the end, you get a warning, seemingly because
Search is run with the warning enabled.
Oh sorry... the location of the warning seems sometimes wrong — it's never attached to
Search, but it seems to the previous statement (even when single-stepping) — preventing
undo from doing its job correctly
Require Import Bool. Require Import ssreflect. Require Import Lists.List. Definition foo := 1. Search "++".
Why not report this as a bug?
ack. filed https://github.com/coq/coq/issues/13637; not a great report but better than nothing
Last updated: Sep 26 2023 at 11:01 UTC