coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Patricia Peratto <psperatto AT vera.com.uy>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Library NOrder
- Date: Thu, 20 Oct 2016 19:02:17 -0300 (UYT)
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
- Dkim-filter: OpenDKIM Filter v2.9.0 mta01.in.vera.com.uy 21B87221BD7
- Ironport-phdr: 9a23:/gWhYhaECyYWRBBWAxdodZn/LSx+4OfEezUN459isYplN5qZpc+/bnLW6fgltlLVR4KTs6sC0LuM9f2xEjRcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3p7xirH5o8GbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWdQKT/HoXU2xeqhdSChTZ61muRozpvzHzqvZ68DeXJ8SwRrcxHymzufQ4ACT0gTsKYmZquFrcjdZ92fpW
I want to use proofs from the Library NOrder.I get the message:Error: The reference le_0_r was not found
in the current environment.The same with other proofs.Is there other library that includes the proofs of NOrder?RegardsPatricia
- [Coq-Club] Library NOrder, Patricia Peratto, 10/21/2016
- Re: [Coq-Club] Library NOrder, Laurent Thery, 10/22/2016
- Re: [Coq-Club] Library NOrder, Yves Bertot, 10/24/2016
Archive powered by MHonArc 2.6.18.