coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] determine the resolution of imports

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] determine the resolution of imports
Date: Tue, 14 Feb 2017 15:39:51 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f178.google.com
Ironport-phdr: 9a23:VPli3hxW3tnxhF7XCy+O+j09IxM/srCxBDY+r6Qd2+oRIJqq85mqBkHD//Il1AaPBtSGraocwLOP7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhDexe69+IAm5oQnMq8UbgZZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8JwgqxVow+vqQJjzIPPeo6ZKOBzc7nBcd8GR2dMWNtaWSxbAoO7aosCF/YMMv1Yr4n8vFsOrQWxBQqxD+7zzD9HnHn20rAn2OkmCw7JxwwgH9MVsHTUstr1N70eXvqzzKbSyzXMcula2Tb86IjUfRAsuv6MXbdqfsrQzUkjDR/KjlKVqYH8OT6ey+oDs2+e7+V6VOKvjXYqpB12oji1wMcjlI3JhoYPxl/a6Cp53YA4LsC7Rk5jedOoDodcuiWAO4Z1Qs4uWX9ktDgmxrEcpJK2fisHxZI6zBDFcfOHaZKH4hf7WeaRPzh4gHVldaq6hxmo8EigzvTwVtC30FpWtyZFnMTAu3IO2hDJ5ciHTfx9/kil2TmRzQzc9uZEIUUsmaraLZ4u3KIwm4INvUjfGiL6gkb7ga+Mekk65OSk9/7rbqjkq5KfL4N0jxvxMqUqmsyxG+Q4NQ0OUnCB9uun1L3j/Fb5QLVUgf01iKXWqpbaKt4dpqGkGQNV04cj6wqwDzq939QYmGMILFNBeB6dk4fpPFTOLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g4gZQCeEBrKTePfZtkbN7eYyKcGNYpUUsXDzMa52yeTpiCoQk18cZqmk3tM+bnm+ErwyKk+ZYGHsj9RHGGEDuAZ4Te32h3WNVDdSYzC5WKdqtWJzM56vEYqWHtPlu7eGxiruRpA=

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/

[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