Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] fully qualified names in Print Assumptions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] fully qualified names in Print Assumptions


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] fully qualified names in Print Assumptions
  • Date: Wed, 10 Jan 2024 22:04:44 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oo1-f48.google.com
  • Ironport-data: A9a23:l8wLGaDbtRk2xxVW/+bmw5YqxClBgxIJ4kV8jS/XYbTApGx01GZUy mQZDTvQbPreMWCgKNF0OtjjoBkEu8LQyIBiOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHZDdJ5xYuajhIs/va8Es21BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc51DqU1rq2NFxNkpsOook4uxbK1p1r 9VNfVjhbjjb7w636LeyS+0pgcN6ace3bMUQvXZvyTyfBvEjKXzBa/+StJkIgXFp2JkIQaa2i 8kxMVKDaDzCagZIPFgND4klzc+ng3D+d3tTr1f9Sa8fujSOnVMpgOa3WDbTUtGgGelzgW2Un Fn54EfACQk8NYag+CXQpxpAgceKx0sXQrk6H7qhs/VunVe73X0WEBRQVF2hoPD/hFTWZj5EA 0kd+y5rqq9rsUL3Hp/yWBq3pHPCtRkZMzZNL9AHBMi24vK8y26k6qIsF1atsfR/7JVoFw85n ESEhc3oDjFJubiYAyDVvLSNoD/4fWBfIWYebGVWBUEI8vvykrEV1xjvd9dEFLLqr9vXHTqr/ SuGghJjjJoujOkK9Z6Bw3b5vxyWqKPkdDUFvjfsYjr97ydSRpKUWIiz2F2KsddCNNm4S3eCj lglmu+fzuYEMr+VngfQQu9XRLCNzNSGOQ36nlRAMcQA9TOs2nj7ZqFWwmh0C3lIO/Y+Ww3CQ RHsqyIIw7RMLl6GULRRX7uhL+gLkY3xCsXDVN3PS9hFP6hKaw6M+R9xaX6q32zClFYmlYc9M 8y5dfmAIGk7C6N16iifXMYYjKEWwx4hyVPpRZzUywqt1ZycbiW3TZYHKF6/UfAr3piboQn68 8dtCOXS8k9xCNbBWyjw9ZIfCXsoLnJhXJD/lJFxR965ewFjHDksNu/VzbYfYLdapqVylNrT3 3SDS0RdmUveh3rGFF2wUUpdSojTBLRxkXFqGhYXHweM+2MiaoOR/qsgZ8MJXb04xtdCk99wb dc4IvulPNoeaw766ww8bIb8prNMbB6EpxyDFAv7bSkdf6xPfR3o+NjldDTB7CMlVzS9p+Yik b+ZiifeTYQJHQh5Pv2Lavj1l1KVlloekdJUQEHnDIRyekLt0Y4yMA33rKY9DP8tICX55Amx9 lipEzIHg+jSsqkJ8NXtroKVnbeDSudRMBJTIDjG0OyQKyLfwFuG/aZBd+S5JRbmS2L+/fSZV 9V/lv3THqUOowdXjtBaDb1u8KMZ4unvrZ98yiBPPi3CT3avO4NaDki25+t9nYwT+eYBoiqzY FyFxfdCM7bQOM/FLk8YFDB4Usu9j8MrihvgxtVrBn7l5R1H3quNCmRTGBiutBZzDpVINKEd/ ONwn/JOtiKejEIxP8eknxJk0T2GDkY9XpUNsrAYB47WiTQX9GxSXKyENAjI5MCgVtYdFGgrP T6eu4TajZt+2EfpUiQ+BFrN78VnlLUMvxF4lgYCLmuWh+uf1+MW3QJQwxszXA963hVK6MMtG 2lJZmleB7SCwCdsv+dHB1uTIgBmAAaI3HD+0H4bvTT9Y3Twc1fSPUoRHP2o/nEJ1059JR9lp Kq5zkThWhbUJPDB5DM4AxNZmqayXO5P+R3ns+H5OtaOAL0RQyfv242qbko28yrXO9s73hD7l LM77dRLSPPJMAALqPcGEKic77MbTS6EKEFkQf1M+KAoH3nWSAqt2AqhelyARcdQG8PkqUOIK dRiBsZqZSSM0CyjqjM6B6lVB5RWmPUvxsQJe5K1BGognoackAFUs8PrxnCjvFMoftRgr59sY MeZPTePCXeZinZoinfA5psMcHaxZd4fIhbwxqap+eEODIgOq/xobVp06LavonGJK0Fyynp4Z u8Yi3P+lISOCLiAnrcA1o1GDgSwbNT0DaGGrFD1vNNJYtfCd8zJsmv5b7Uh0xt+ZdMstxZfz Nxhc+IbGGvKub83VybSnJzp+2xh+5CpROQOWi7oBCAyoMZBMfMAJzMM/mm5LdpCl9Y1CgxLg eenQJPYSOP5kOuxCJGYh+ay3vrd52nKgn/cmB6A
  • Ironport-hdrordr: A9a23:a1J9065g7d+D2ekjrwPXwPHXdLJyesId70hD6qm+c3Nom62j5q WTdZsgvyMc5Ax9ZJhko7G90cq7MBHhHPxOj7X5VI3KNGLbUSmTTL2KhrGSoAEIbheOj9K1op 0QFZSWZuedMbEDt7ec3ODuKadF/OW6
  • Ironport-phdr: A9a23:XwcgOBFTX9Kpo0RO0c+t+p1Gf+FGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k33BmTA9yQsq8ew8Pt8IneGkU4oqy9+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCS+bL9oM hm7rBjdusYLjYZiNKo61wfErGZPd+lKymxkIk6ekQz76sms4pBo7j5eu+gm985OUKX6e7o3Q LlFBzk4MG47+dPmuwDbQQSA+nUTXGMWkgFVAwfe9xH1Qo3xsirhueVj3iSRIND7Qqo1WTSm6 KdrVQPohSIaPDM37G3blsp9h79drRm8pRJw3pTUbZmaO/pwfKzTfd0US2lcUMhPSyNMGZmzY 5cVAucbIepUs4vwql0TphW+HwmsA+bvxydMiHDsxq061OIhGhzH0gw6GNIOq2/Up8jyOacQS ++1167IzTPMb/NM3jf985PIfxQ6rPGDWLJ/a8vRyU01GwzZiVWQrJXoMjWI3esCr2aV9fBvV f6zi2E5sQFxpCCiy8MihITJmo4YxUzJ+CV5zoorK9C1S1B3bMC4HJZeqyyXNo97T8wtTW10p is0yr8LtJ+7ciUF1JkpyB3SZfKZfoWO/xntWuGRITJii3JkfrKynwq98U+6yu36SMa01FJKo jBbndbRq3AA0QHY5MufSvZl4EutxTKC2xrQ5+xEO0w4iKvWJ4M7zrM/lZcet1nIEzHymEXrl 6+Walsr+vK15eTmY7TpuIeRO5NyhwrjKKohgNa/Dv49MgUWX2iU5+C81Lr78E38WrpKj/k2n rDesJDdOMgXv6C5DgBW34o55Ba/CDCm0NscnXYZNl5KZBWHj43xN1HPJvD3E+u/jkyynDt3w /3KJL7sD5XXInTekbrtYKxx5kFfxQYryNBQ/ZNUCrUPIPLpXU/xscTVDh0jPAyvxObnDtp91 pkZWWKUGa+UNLjfsVCN5u01IumMYJUZtyr6K/gg//Lui2Q2lkcHfaa1xZsXdGy4HvN+LkmEe XbsmMsOEX8WvgoiS+znkEGNUTlKZ3qrQ6084iw7B5m9AIfYRoGthaSB0z2hEp1XYGBGEFGMH m3ye4WKQfdfIB6Vd8Rmi3kPUaWrA9sq0gjrvwvnwZJmKPDV82sWr8Sw+sJy4rjxnAo183RbF cOGyCnZTWhvmWUHXTgtx/FXrkl0y1PF2q991a8LXedP7u9EB19pfaXXyPZ3XoiasmPpe96IT AzjWdC6GXQrSdl3xdYSYkF7EtHkjxbZ3iPsDaVG36eTCskS9aTRl2P0O94702zPgasolF4gT dFILnb3rqF6/gnXQYXOlhbRjL6kIJwVxzWF72Kf1SyLtUBcXhR3VPDHVGsYYETMqs/it2vNS ravDfIsNQ4SgdWaJP5sbdvkxU5DWO+lONnaZDepnHysAB+T2r6WRI/jemFY2yKETUZYw0Yc+ nGJMQV4DSCky47HJBppE1+nI0bl8O0k7Wi+Uldx1QaBKUtoy7uy/BcRw/2aUfIamLwe6m8nr H1vEVCx0sizaZLIrhd9fKhafdI24UtWnWPfuQtnO5W8LqdkzlcAegVztknq2l15EIJF2cQtq XorykJ1J8f6mBtDfiif25/qPabMe0H9+Rmub+jd3VSfmNea96ET6egp/k35tVLhHU4j/nN7l thNhiHEt9OaUUxLD8u3DhZkknoy76vXaSQ8+Y7OgHhlMK3u9yTHx8psHuwujBCpY9ZYNqqAU g70CcwTQca0e4lI0xCkaAwJOOdK+es6JcSjIrGE0bWsOul6mym93ExI5Yl81gSH8C82GYuql 94VhuqV2AeKTWK2jl66tcb4g4dffmA6EW+2yCyiD4lULP4XH85DGSKlJMu5wc97jpjmVitD9 VKtMFgB3degZRuYa1GVMRR47U0MujTnnCK5y2YxiDQ1tu+F2yeIxe3+dR0BM2oNRW94jF6qL 5Lmx9wdWUGpaUAumn7HrQ74zrNcoqtlKHLIEG9HeiH3KydpVa74ureZYsFJ4Y8lqm0NCLX6M Q3cE+Ck5UdKmyr4V3NT3jU6ay2ntvCb11RhhWSRIWwy5HvVdMdsxAvOsdnVRPpfxD0DF2Fzj TjaAET5PsH8p43F0cee9LngDiT9Bs42E2Gj146LuSql6Hc/BBS+m6r2gdj7CU0g1iS90dB2V CLOpRK6Y4/x1q38P/g0GysgTFL69cd+HZlz14Uqg5RFk3oTnZKT8mAAinyiGdpe0KP6KnEKQ HRYprydqBigw0BlIn+Tksj7X26axMR7YMKhM0sZ3ys864ZBD6Lev9km1WNl51G/qwzWe/10m DwQnOAv5HAtiOYMoAMxzy+ZD+NaDQxCMCfrjRjN88GmofAdejO0abbpnhkb/5jpHPSYrwpbQ nq8ZpoyAXo68JBkKFyVmHzrttO/JZ+JPIpV7EHL1U+H1bQdKYptxKRWw3A8YiSk4yVjk6li3 HkMldm7pNTVdTsrpfrjREYebnqvP4sS4m2/0/gYxJrHmdD3WM0mQG1DXYO0H63yVmtO8622b UDWV2RszxXTUbvHQV3AtAE/9S+JS9bzcCjJbHgBkYc7HEnbfRMAxlBSBHJgx9Y4Dlz4nZO6N h4ounZJoAa/80UpqKogNgGjAD2H9UH4N3FtEsjZdF0PsUlD/xuHa5XAqL8jWXgJpNv561XcY m2DO1YSVD9PABfVQQu5eOHpvIilkaDQEOO6K7Gmjaymj+tYWr/IwJuu1tEj5DOQLoCVOXIkC fQn201FVHQ/GsLDmjxJRTZF3yTKJ9WWohux4EgV5oi27ejrVQTz5ICOF6oaMNNh/AqziLuCM OjYjThwKDJR3JcBjXHSz71X0FkXgiBoPz6jdNZI/TbKV77Vk7RLAgQzbipyMI5P6Pt50FUdf 8Hcjdzx2/hzift0Q1ZJWFr9m924MMwHJ2buUTGPTE2PNbmAOXjK25StOfL6GeAW1bsN8UHg6 lP5Wwf5Mz+OlifkTUWqOOBI1mSAOQBG/Zu6eVBrAHTiS9Tvblu6NsV2hHs42+5R5DuCOGgCP Dx7a04IoKeX6HYSgPxkHGpO9H1+NrislCOQ7u2eIZET+6gOYGw8h6dB7XI2xqEApjlDX+Bwk TDOo8RGplinlqyIzWMiXkYe7DlMg42PsANpPqCTpfwiET7UuRkK62uXEREDodBoX8but65nw d/KjKvvKT1G/ro8GOMTAsHVLISMN39zaXIB+RbRBQoBCDmsbCTR2xwbn/aV+XmY6JM9r8q08 HLhYrBeXV0xUPgdDxY8dOE=
  • Ironport-sdr: 659f1491_TM5fwh2RV3CdAhWAoM8qs1+jFlKpPD6tLE2lcJKUEgwCeUq xsoIO24e8vHmlm2HBS5f4HUcnEfdsgTp7eeQZig==

Probably not the solution you're looking for, but if you `Print Assumptions` from a file with no `Import`s, only `Require`s, you should get fully qualified names.

On Wed, Jan 10, 2024, 16:24 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
Is there a way to get Print Assumptions to output fully qualified names of all items?
That could help in filtering in/out items.




Archive powered by MHonArc 2.6.19+.

Top of Page