coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] query to print topfile
- Date: Thu, 18 Jan 2024 17:29:48 -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-wr1-f49.google.com
- Ironport-data: A9a23:MRct5Kl1ja1bUHPNs/ApYVXo5gwnIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIWWT+Ba66NY2umKN8lao7n8RgE6MXWxtJnHlRoqixhRltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayaj98B56r8ks14Kyr4WNA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1+BhAGO4BGxdpyKkV2r c4IOG4nUlOc0rfeLLKTEoGAh+wmJcjveZwF4zRukWCfAvEhTpTOBa7N4Le03h9q3pEITauYP ZBAL2Y+BPjDS0Un1lM/AZg+nfyoi3q5ejtRrl7TpKsr7EDcyQVw1P7mN9+9ltmiGpoPxB/E/ TOuE2LRWQoWLP286wC8yWuTi+mUtynjdoIbC+jtnhJtqAbOnzRMWUN+uUGAifK+kwu1X89VA 1cF/zIn66k07k2iCNfnNyBUu1aBtx8YHsVKSqg0tFDLxa3T7AKUQGMDS1atdeDKqucmT20a0 FLXoO/sLhhX6I+FWSy3yvSL+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOP7l5jESMWGvq w1mvBQDa6MvYdnnPphXEHjCijOo44fTF0s7ulSRUWWi4Qd0IoWiYuRECGQ3D94Qfe51rXHY4 xDofvRyCshQV/lhcwTTGY0w8EmBvartDdElqQcH82Md3zqs4WW/Wotb/StzIkxkWu5dJme0P heJ51wKu8MDVJdPUUORS9LhYyjN5fi/fekJqtiNMbKin7AoKFHeonkwOSZ8IUi2zxZ1yMnTx qt3ge73UC9CVvU5pNZHb+ga1rAvy2g/w2iVLa0XPDz2uYdykEW9EO9fWHPXNr5RxPrd/G39r YwDX+PUkE43eLOlPUHqHXs7dgxiwY4TXs2u96S6t4erfmJbJY3WI6GKn+J+J9A+wcy4VI7gp xmAZ6OR83Kn7VWvFOlAQikLhGrHBM4l8yAILmY3MEy22nMuR4+q4e1NP9E0ZLQrvqgrh/J9U /BPKY3KD+VtWwb33W0XTaD8i4h+KzWtpwaFZBS+bBYFIpVPeg3u+/3fRDXJyhUgNCSMmPEFk +WS7T+DGZsnbCZ+PfnSc8Oqng+Qv2BCuedcXHnoA9h0eWfq+rdEMyba0/09eZkNDT7hxTKq8 RmcLjlFhOvKoq4zqMLog4LdpaiXMuJOJGhoNEiF0qSXbA7x4XiG7bJbdtqxbRTxdT/R6bqzQ +d41NT+O6A3p0lLuI9CDLpb96IyyN/xrbt8zA4/PnH0Q3m0K7FnMF+U9NJus/BT+7pnpgeGY EKD1d1EM7GvOsm+MlowJhIgX9uTx8MvhTjewvQkEnrUvBYt0uK8bnxTGB2QhAh2Drh/atoly Nh8nv8m0VW0jx5yP+uWiixRyX+3EUUBdKcarbAfPp7gj1s661NFYKGEMBTM3rO0V4xuPHUpc xiuv4iTo5RHx0HHTWg/KmiV48pZmqY1mU5ryH0sGg23v+Tr19EL2C9fyzAVdjhu7w5m1rtzM 1d7NkcuKqSp+Sxptfd5XGutOl9gARGFy3P10H8MsnPTdGizd2n3NGZmE/28zEMY1GN9fzZg4 7CTzlj+YwvqZM3c2igTW1Zvjv7eEfhd0xLko9/+OeioBLw4bijBro70QFEXuj31Bc8Vr2/Wl 9lApepfR/XyCn8NnvcdFYKf64U1dDmFA25nGtRK46IDGDDnSgGYgDShBRi4RZJQGqbs70S9N s1JI/BPXTSY0AKljGgSJYwIEo9OsM8Z3vgwUZK1GjdeqJqalCRjj7zI/CunhGMLfcRnofxgF qzvLQC9Ak6irloKvVTSrft0GHuyOvgFQwze4Nqb0ss0E7A7jeU9Vn1qj5WVuS2OPRpF7iCkm lrJR5XrwtxIzaVumIrREZt/OTikFOOrVMq03VCyl/9sceLwNdz/slJJi1v/YCVTE7gje/V2s rWvrO/I2FjhjLondluAnr+tFLR7v5SsbrBHNubyCmdQpgqZecrW+xBY0XuJGZ9It9J858ecW AqzbvWrR+MVQ9twwH50aTBUNgQ0UYDbT/7Hi3umjvKuDhM971T2HOm//yW0UVABJz46BZLuL yTV5dCs34l8h6ZRDkYmA/pGPcdJEGX7U/F7S+yr5CiqNUj2sFasobC4qAEB7wvMAXy6EMrXx 5LJaxz9VRaqspHz09BrnN1ujyITEUpCr7E8TmAF9/5yrgKKPmoMAOAeEJcBU7V/sCj50rPmb zDsMkomLwjAXgp/TBat2+S7Az+jBdEPNOmgd3ZttwmRZjytDYyNPKp5+20yqz1qcz/k16e8J ctY5nT0OQOrz4p0QfoIoMa2mvpj2uiQ00dgFZoRSCAuK0127XQ2OH1d8M5lUCXGF4TSjhyOK zRkA29DR06/RAj6FsMIl7u53v0GlGuH8tnqRX7nLBXjV0Gzw+hJyfm5MOb2ulHGRNpfP6YAH BsbWEPUi117GRUvVW8BtNcggKsyAvWOdiR/wGkPWiVK95yNBq8b0w/uUMbBoAzOOOKSLr8Fq gSR3g==
- Ironport-hdrordr: A9a23:rOCAqaDqpWhtFgjlHemh55DYdb4zR+YMi2TDtnoBLiC9F/bzqy nApoV56faZslYssRIb+OxoWpPwI080nKQdieIs1NyZLWzbUQWTXeVfBEjZrwEI2ReSygeQ78 hdmmFFZuHNMQ==
- Ironport-phdr: A9a23:V8/y/hfr45NXCEa26UUV7qf4lGM+9tfLVj580XLHo4xHfqnrxZn+J kuXvawr0AWZG9+Eu7kd0LGempujcFJDyK7CikxKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf7B/I A+ooQjTtcQajpZuJ6g/xxDUvnZGZuNayH9nKl6Ugxvy/MC88oJ9/S9Nofwh7clAUav7f6Q8U 7NVCSktPn426sP2qxTNVBOD6XQAXGoYlBpIGBXF4wrhXpjtqCv6t/Fy1zecMMbrUL07QzWi7 6NsSB/1lCcKMiMy/W/LhsBsiq9QvRSsrAF9zYHJeoGYLPVxcKPTc90ZWGRPQNpeWjdbDY+gd YYCFfYNMfpaooT7ulAArQG+BQ6pBO731jJHnX/23awh0+QhDw7G3xErEs4IsHvOqtX6KboZX Oevw6bTzTXDbuhW2Tfj54jLaBwuu/eMUqh2ccXM00UvFgLFjkmfqYH+MDOV0/4Cs2mf7+Z6S e2vjGsnphh3rzOyycgilpPHiZgJylDY6yp52oA1KMW5RUNmYdCpE4dduz2aOoZyTM0vQ25lt Do7x7EbuZO2YCwHxZs6yhPCaPGKc4aG7B3/WOuSLjp0mH1rdryhihi990Wr1+PyVs6x0FlQr ypFlMHBuWoX2BDJ8ceIUeNx8Vum2TaV0QDc9OVEIUQumaXFNpEh37g9nYcQv0TbBiL6hln6g auMekgn+uWk8frrbqv7qpOGOIJ5jgfzObkwl8y7HOQ4KRQOUHaB+eqh1b3i/FP2Ta1WgvAwj 6LXqorVJd4Bqa68GwJV0pgs6xK4Dzq+1dQXh3gHLFZcdBOJlYjlJkjCIP73APq7mVisnzBrx /fJPr3lHJrBNGTMkLDkfbpl6k5czhQ8zcxH6p5KFr0MJOj/V0zxudDCEBM1LRG4z/zoBdh5z o8eXHiAAq6dMKPcq1+I4ecvLvGWa4AOuDb9KuMl5/7wgn86g1MSZ6+p0oERaH+lBPhmIkSZY WbjgtoaHmcKuxAxTO3uiFGYTTFTYHOyU7o65j4gEI2mF5vMRpixgLyd2ye2BoBaanhcCl+QC Xfoa5mEW/AUZS2OJc9hiyUIWqSlS488zh6jrxT6yrpiLurM4CIUr5Pj1N5v5+3Sjx4+7zJ0D 97Om12KGmpzhyYDQyI8lPR0plU4wVOe24B5heZZHJpd/aUafB09MMv1xex7END/WUroeN6PR B7yS9+mACoxQ9F3ytkHZUo7GtS+gTjM2iOrB/kekLndV898yb7Vw3Wkf5U18H3BzqR01zHOI +NKPGyi3etk8hTLQpXOiwOfnrqrcqIV2GjM8n2CxCyAphIQSxZ+BIPCW31XfU7KtZLh/EqXR rWuCK8nPwgHwMiLLKcMa9z1gn1JQf7iPJLVZGfi03yoC0Owz6iXJJHvZ31b2SzcDEYelAVG9 HyGNBM+CyTnqmTXCjAoFFPzbGvj9OB/rDWwSUpnhxqSYRhH0Ly4sgUQmeTaS/4X2eccvzw9r jxvAFun99ffCt7FuBA4OasAMJUy51BI0W+fvAt4VnC5B4ZlgFNWMwF+vke1kg5yFp0Fis8y6 nUj0At1L6ucllJHbTKRm57qaPXRLSHp8RajZrSzuBmW2cuK+qoJ9PUzqkny9ACvGE049nx70 t5Tm3KC75TOBQAWXNr/SEEyvxR9orjbZGE66ea2nTVlO6m1qT/P2JQgAuIjxlChfstQGKyBH Q72VcYdAonmKeAnnUSocgNRJPpbp8tWd4utc/qL3rLuPf41xmr3yzQaptoniwTQpnkZKKaAx ZsOzvCG0xHSUj79iAzkqcXrgcVfYilUGGOjyC/iDYoXZ6tofI9NB339Rq//jth4mZPpXGZVs VC5AFZTksajeRuJb1H+mwRW3EIb532mhSSQwDl9kjVvpa2aln+roayqZF8cN2hHSXM3x17mI Ymvj90ZGkGuZg4l0hqk+UnSyK1SpaA5JG7WCxQtHWC+PyRpVa2+saCHashE5cYzsClZZ++7Z EiTVr/3pxZyPzrLJ2JF33h7cjirvs68hBlmkCeGK241qnPFeMZ2zBOZ5drGRPcX0CBUDCV/j DDWABC7MbzLtZ2dnZfCqeCzVCSoUJRVfW/qzJ+PnCS+7GxuRxa4mri/l8bmHg4zzSLgn4MyB GOY8VCmONCti/XyOPkCHAEgHFLm7stmBoxy2pA9gp0dwzlSh5mY+2YGjXamNNxa3azka39eD TUPwtPT/E3kwBg5diPPl9+/DC/EhJcwNLzYKisM1ykw7t5HEvKR5b1Axm5up0ag6BnWeb57l ysczv0n7DgbhfsIsUwj1Hb4YPhaEE9GMCjrjxnN4cq5qfAdbWyvcKOw2Uk4lNaoCr3EowBAV 172f54jGWl76cA1YzeumDXjr5rpftXdd4dZvxeUkgzAgusTIZQ4kPZMhCt7NkryuHQkz6gwi hkkjvTY9MCXbm5q+qy+GBtRMDb4MtgS9j/ahqFbhs+K3oqrE8YpCnARUZDvV/7tDCMKuKGtK VOVCDNl4CT+e/KXDUqF5UxhtX6KD527KyTdOiwC1ds7DBiFeB4E3UZNDW18xMJmUFjtnpCpc V8ltG5NoASj8V0VlLoub16mAwK97E+pcmtmFsbZdUIMqFkEvwCPaYSf9r4hQX8epMHw6lzVb DTcPVwADHlVCBPeQQm/eOD/v5+YtLHIY4j2Z/rWPefR9aoHDarOndT3ldI4tzeUapfWZikkV qJknBoFBTcjQozYg2ldEnNM0XucM4jD4k/7o3MSzIj38ey3Cli3tM3fVv0La4Upo1fv3u+CL 7LC3n8nb2sIkMpdnzmQj+FOlF8K13M0LmfrS+9R83WXCvqXw/4ybVZTfSp3MIEgA7sU+A5LN Iabj9r00uU9lfspExJeUkSnnMi1ZMsMKmX7NVXdBU/NOq7UbTvMi9r6Z6+xU9gyxK1dqgGwt DCHEkTiIiXLlj/nUAqqOP1NiyfTNQJXuYW0eBJgQWb5S9euZhq+Od5xxTo4pN98zmvNLnIZO CNgflllq7SR6WZHmKw6FTAQqHViKuaAlmCS6OyZYpcavP13AzhlwuJX5HNprtkdpCpARfFzh G7Ttos0+wDgwrTJkGA+FkYf+VMpzMqRsE5vOLvU7MxFUHfAp1cW6HmITg8Nv51jA8HuvKZZz p7OkrjyIXFM6YGxn4NUCs7KJcaAKHdkPwDuHWueBQEFTCWrOGKZjkpUlv3U93yJobA1r5Htn NwFTboRBzlXXrsKT19oGtAPOsI9RjQ/jbuSl9IF/1K7pRjVAdpA59XJCqPUDvLoJzKUy7JDY lFbpNGwZZRWPYr91Ut4b1B8l4mfAEvcU+dGpSh5ZxM1qkFAmJCfZmg62kagdRn0pXFPRLi7m Rk5jgY4auMopm+EC7IfKV/DpS92m040y42Nad+5fzv4LaP2VoZTWXOcig==
- Ironport-sdr: 65a9a680_JQ5/9iuGsrbkad36OrOjOTfGe8vGwva+xdzPNuugyAwufci /AWAhMcPqGo1uagvRhC/tfU3NgB6LVzN53bZXsw==
Is there a Coq query to print the fully qualified name of the current file being compiled or checked interactively?
For example, consider the setup:
[abhishek@optiplex tempp]$ cat tes.v
Definition xx:= 2.
Locate xx.
[abhishek@optiplex tempp]$ coqc -R . aa.bb tes.v
Constant aa.bb.tes.xx
For example, consider the setup:
[abhishek@optiplex tempp]$ cat tes.v
Definition xx:= 2.
Locate xx.
[abhishek@optiplex tempp]$ coqc -R . aa.bb tes.v
Constant aa.bb.tes.xx
If I replace `Locate xx` above by the supposed query, say, PrintTopFile, it should print
aa.bb.tes
aa.bb.tes
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] query to print topfile, Abhishek Anand, 01/18/2024
- Re: [Coq-Club] query to print topfile, Gregory Malecha, 01/20/2024
Archive powered by MHonArc 2.6.19+.