coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vadim Zaliva <vzaliva AT cmu.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Library Coq.ZArith.Zlogarithm
- Date: Wed, 1 Apr 2020 11:24:57 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-io1-f47.google.com
- Ironport-phdr: 9a23:nV63thC2HDdD7+peHaFGUyQJP3N1i/DPJgcQr6AfoPdwSPvzoMbcNUDSrc9gkEXOFd2Cra4d1qyO6eu5AzZIoc7Y9ixbLNoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6Y8xgHVrndWdOha2H1kKUyOlBr4+su84YRv/itNt/8u7cJMTbn2c6ElRrFEEToqNHw468LsuRTfVwWE+2ESUn8RkhpGAgjF6A/1U5LsuSbkteRzxTeXM9TuQb87RTqt4aFrSAT1iCgcLD427HvXis1rg61Fph+qugFyzJTVYIGRM/p+Y7/dcNYHTmdPQspdSypMCZ66YoASDeQOIPxYopHyqFUOoxWwBhSiCv3zxTJTnHD6wbc33v49HQ3a3gEtGc8FvnTOrNXyMacfSe+6w7PVwjXCavNdxDTy55LMchAgv/GDR697fM3PyUguDQzFilSQqZL/MD6OyusNtnWb4/B+Wu2ylm4qsgd8qSWhyMcrj4nGnIMVylbc+CV/2ok1IMO3RFdnbt6jCpRfqyGaO5FqTcMlRmFlvjsxxL4euZOjYiQG1JAqywTcZvGHaYSE/xPuWeeLLTp3hn9ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrnUN2AbS6siDU/d9/0Ch1SuW2wDd5exJI1o4laXcK54mzb4wkoQcvV7fES/xnUX6lK6WdkM69ei08+nrfKnqq5uGO4J3igzyKLkil82+DOgiPQUDXXCX+eGm273i+U35Tq9KjvozkqTBrpDVP9kUpq+8AwNP04cs8RK/Dza40NsChnQGIkxKeAmbj4TzJ17OJe34Ae2hjFuxjTdn3+rGMaH5ApXRMnjDl6/scqp6605F0QY80dRf549PBbwaO/LyWkrxtMTCARMjMgy0xfznCNRn2Y8EV2KPGPzRDKSHuliRo+krPuOkZYkPuT+7JeJ2yeTpiCoHkFMceOGb1J8WdnnwSup0KkGYf3PEidIcV2oGo1xtH6TRlFSeXGsLND6JVKUm62RjUdP0PcL4XomoxYe58mK+F5xSaHpBDwnQQ2jlbJnCUPIRLi+eP504y2BWZf2aU4YkkCqWmkri0bM2fOHR52sVuY+xjIEotd2Wrgk78HlPN+rY02yJSDspzGYBRjtz3acm5EIhlRGM1q93h/EeHttWtatE
The library Coq.ZArith.Zlogarithm was deprecated and was removed in 8.11. However, I have proofs depending on it and I could not find some lemmas which were there before. For example: Psize_log_inf, Zlog2_log_inf.
What is the recommended solution for this?
- [Coq-Club] Library Coq.ZArith.Zlogarithm, Vadim Zaliva, 04/01/2020
- Re: [Coq-Club] Library Coq.ZArith.Zlogarithm, Vincent Laporte, 04/02/2020
Archive powered by MHonArc 2.6.18.