coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] determine the resolution of imports
- Date: Tue, 14 Feb 2017 21:50:09 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Pass smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
I would look at coqdep's output.
Gaëtan Gilbert
On 14/02/2017 21:39, Abhishek Anand wrote:
I am trying to debug a mis-resolved "Require Import ...".
Is there a way to see the exact location of the .vo file to which the import was resolved to by coqc/coqtop?
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/%7Eaa755/>
- [Coq-Club] determine the resolution of imports, Abhishek Anand, 02/14/2017
- Re: [Coq-Club] determine the resolution of imports, Adam Chlipala, 02/14/2017
- Re: [Coq-Club] determine the resolution of imports, Gaetan Gilbert, 02/14/2017
- Re: [Coq-Club] determine the resolution of imports, Hugo Herbelin, 02/15/2017
Archive powered by MHonArc 2.6.18.