coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Randy Pollack <rpollack0 AT gmail.com>
- To: Coq-Club Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Anomaly: Uncaught exception Not_found. Please report.
- Date: Mon, 23 Jan 2017 17:56:57 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=rpollack0 AT gmail.com; spf=Pass smtp.mailfrom=rpollack0 AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f176.google.com
- Ironport-phdr: 9a23:c+70BB9x8NShbP9uRHKM819IXTAuvvDOBiVQ1KB90uocTK2v8tzYMVDF4r011RmSDNmdt6MP0rKK++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Dq3PF4XTl8W60fyps92WOl0QxWn1XbQnBxKv6C7Vq8Neqo9/IO5lwRzQ53BMZu5+xGVyJFvVkQyqtemq+5s2yS1Wt+Npz8lEVazxfOxsV6RfCDAvOGNtzMLuvBjHCwCI4y1PAS0tjhNUDl2dv1nBVZDrv36/77Il1Q==
Consider the following two files. Coq 8.5pl1 with ProofGeneral fails
to load file_XXX.v
The definitions are just to make the example non-trivial, but the
[Require] seem to be relevant.
BTW, I tried to log in to Bugzilla, but failed.
--Randy
=====file_XXX.v=======================
Module XXX.
Require Bool.
Load file_YYY.
Export YYY.
Definition tt := true.
End XXX.
=====================================
------file_YYY.v---------------------
Module YYY.
Definition ff := false.
End YYY.
--------------------------
- [Coq-Club] Anomaly: Uncaught exception Not_found. Please report., Randy Pollack, 01/23/2017
- Re: [Coq-Club] Anomaly: Uncaught exception Not_found. Please report., Hugo Herbelin, 01/25/2017
Archive powered by MHonArc 2.6.18.