The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Dear Coq users,

We (the  Coq developers) would  like to remove the  Correctness tactic
from Coq's distribution,  since it is wholly subsumed  by the Why tool
(http://why.lri.fr/).  Before doing  this, however,  we would  like to
check if it is not still used by some Coq users. If so, please send me
a note (personally).

Best regards,
-- 
Jean-Christophe Filliâtre