Stream: math-comp users

Topic: Removal of ssrsearch


view this post on Zulip 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).

view this post on Zulip Florent Hivert (Sep 23 2021 at 19:21):

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

view this post on Zulip Enrico Tassi (Sep 23 2021 at 19:30):

CC @Erik Martin-Dorel

view this post on Zulip Pierre Roux (Sep 24 2021 at 09:36):

The Coq (new) one.

view this post on Zulip Reynald Affeldt (Sep 24 2021 at 10:36):

I am not using ssrsearch anymore but keep on forgetting to write inside instead of in :-/

view this post on Zulip Enrico Tassi (Sep 24 2021 at 10:43):

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


Last updated: Jan 29 2023 at 18:03 UTC