Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Library NOrder

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Library NOrder


Chronological Thread 
  • 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?
 
Regards
Patricia



Archive powered by MHonArc 2.6.18.

Top of Page