Enrico Tassi (Sep 22 2021 at 08:57): Enrico Tassi (Sep 22 2021 at 08:57):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).
Florent Hivert (Sep 23 2021 at 19:21):Which one is used automatically by Proof-General when typing ctrl-c ctrl-a ctrl-a ?
Enrico Tassi (Sep 23 2021 at 19:30):CC @Erik Martin-Dorel
Pierre Roux (Sep 24 2021 at 09:36):The Coq (new) one.
Reynald Affeldt (Sep 24 2021 at 10:36):I am not using ssrsearch anymore but keep on forgetting to write inside instead of in :-/
Enrico Tassi (Sep 24 2021 at 10:43):https://github.com/coq/coq/issues/14930
Last updated: Jan 29 2023 at 18:03 UTC