Dear @all , are you still using the old `Search`

command (the one you get with `Require Import ssrsearch`

since Coq 8.12)?

If so, please speak, otherwise we can give green flag to the plan of removing it in Coq 8.15 (see https://github.com/coq/coq/pull/13760).

Which one is used automatically by Proof-General when typing ctrl-c ctrl-a ctrl-a ?

CC @Erik Martin-Dorel

The Coq (new) one.

I am not using `ssrsearch`

anymore but keep on forgetting to write `inside`

instead of `in`

:-/

https://github.com/coq/coq/issues/14930

Last updated: Jul 15 2024 at 20:02 UTC