Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] fully qualified names in Print


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] fully qualified names in Print
  • Date: Thu, 30 Nov 2023 22:57:04 -0500
  • Authentication-results: mail2-smtp-roc.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-wm1-f51.google.com
  • Ironport-data: A9a23:QrCqrKvtQvXMI0w48LrtcJxSCefnVIFbMUV32f8akzHdYApBsoF/q tZmKWyBMq6MYmrzLop+bI3g8ExTvsfUz9U2GlBvqns2FSJBgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRMt8pvlDs15K6p4WpD5gRlDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJEtoJLMT39RWOHhht v81NBQoSA+n2MvjldpXSsE07igiBMziPYdapXQ5iD+EVLApRpfMR6iM7thdtNsyrpoWTLCOO oxAM2opMU2ojx5nYj/7DLo3luepnXnycHtRrluTqew24nTc5AN02bnpdtHSf7RmQO0MxRfF+ z+ZojyR7hcyE/XY2SuM4FmWi8zOjyTUZ4I/KY2Z6as/6LGU7ilJYPEMbnOwpuD8gUqjUfpEO kkM82wvq7Iz/QqlVLHAswaQpXeFulsDXoMVHbBjrg6KzaXQ7kCSAW1soiN9VeHKffQeHVQCv mJlVfuwbdC2mOTNEyzPxaTetj6oJykeIEkLYCJOH0NP4MDurMt3xljDR8pqWvz9xNDkOyDC8 xbTpggHhpIXkZEq0Ye/9gv5mD6CnMXCYTM0wQT1ZVibyD1FSrSrXKGS0miD3818dN6YanKjo Ek7n9Ov6bFSLJOVyw2IbuY/PJCowPenNjfjr0ZlNMQj/W71+lqIX4NZ0BdhLmhHb+cGfj7IZ hfImAVzvZV8AlqjXZVVUamQVfs47PHHPsv3c9zpdfxyW4hVWC7b2TBxdGiS8nvIkkNxoZogO JyeT9mgPUwaBYtj0jCyYeUXip0v+QwT2kLRQoLd3T288L/DekOQd6gJAGGOYs898qmAhgffq PRbFsmSziRgQP/MWTbW/aETPGI1AyACX76ukPNud8mHPgZCM0MiAaWIwboeJqpUr54MneLMp nyASktUzWTkvkL+KCKIV2tCbY3+VpMuvFM5Oi0RZWyT4UYBWrr2zqkjdMoQR4IFpchD1v9/S scXd/qQWspvTiv1wBVDTJ3fgrE7SjGVq1OvBRe1WBk+YJ9qeCLR8PDGYAbE1XcDHwi3h+QEs pyi0QLRfrQbTS87V8zqRe6dzW6hmX0RhugoU1D6GYRRch+08axBCS/4vtkoKe4idDTBwTq70 V6NIBE6/OPina48wOPrt4ul8bi7NvRYH1VLOVXb4ZKdFzjozkD6zaBuCO+3LC3gDkXq86CcV MBp5vDbMsxfum1VsoB5Qo1Z/Yhn6/TB/7ZlnxlZRlPVZFGWC5RlEHmM/e9LkoZvnrZ5mw+Ha nijy+lgG4eiGZ3aSQYKBQ8fcO68++kemWDS4dQLMUzK3nJL04TdY3pCHSunqXJ7F6R0ArMH0 O16mc8x6i6DsDQIHOuCrBhp8zWrEiRdfYQh7ooXEa36uDoNk1tiW6HROgXywZOIauhPDHUUH y+ptPL8oIpYl2X/cCsVNHnS3OBiq4wElzJUwXQjeVmYuNr3qcUm/R9W8AZtFwRc8Qpa4rgiJ klqKExHCqGc9Bh4hMV4fj6NGiMQIDa760DO218yu2mBdHaRV0vJN3wbBemW2VIwqkZwQ2B+x 66J70rAShPoTdHV8gppfnA9sN3lb9h61jOaqfCdB87fQqULO2v0sJGhdU8jikXCE8guoGblu OMz3uJ7SZOjBB4qu6dhVrWrj+UBeiulel5Hb+pqpp4SPGfmfzq35ziCBmaxdu5JJN3I6UWIM NNvFO0eSyWB0DuykR5DCZ4uO7NUmNsb1OgGcJ7vJk8EtOK7hRhtu5Ty6CP/pTEKR/NDrMUDE b7SJgmySjGouXhpmmHz9ZgOfiLyZNQffwTz0dyk6OhDRdpJrOhodlp0ybeu+WmcNAx85R+Po QfffOnswvd/zZh31Z7ZekmZ695Y9fuoPAhJzOyyjziKRdbGMMOLqAZM71e6ZkJZOrweX9kxn rOI2DIyMIUpo55uO101WbHYf0WK2Sl2dOVSO8PzanJdmENunefytgAb9TnQxYNhybtgCwrOe +d8QMS1fN8RHdxawRW5rsSY/wk1U8zKU0srmc9xQzlgxPTQPcwr4e5LLUPUUFw=
  • Ironport-hdrordr: A9a23:PI165K555R1eiAp6TwPXwMXXdLJyesId70hD6qkRc20zTiX8ra qTdZsgpHzJYVoqOE3I+urgBEDjewK/yXcd2+B4VotKNzOW3VdAQrsSibcKAAeNJ8Q9zINgPG tbHJSWweefMWRH
  • Ironport-phdr: A9a23:UGyYQhLVqYFj28uu3dmcuBFvWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFtbM00g+CANSTwskHotSVmpijY1BI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQZFiCCgbb5zL xi6ogXcu80LioZ+N6g9zQfErXRPd+lK321kIk6dkQjh7cmq5p5j9CpQu/Ml98FeVKjxYro1Q 79FAjk4Km45/MLkuwXNQguJ/XscT34ZkgFUDAjf7RH1RYn+vy3nvedgwiaaPMn2TbcpWTS+6 qpgVRHlhDsbOzM/7WrajNF7gqBGrxK7vxFwzI7abo+WOvRjYK3SYcgXSnBdUstLTSFNHp+wY okJAuEcPehYtY79p14WoBaiHgasBOLvyiRIhnDo3q0xzvgsEQfc0wwmAt0FrXPZo8/uO6cSU OC116nIwivAb/9Mwzj97pLHchY8rv2WXLJwcNbRyUY0GgPKi1Wfs43lPzeP2usRtGib6vNtW OSygGEotw9/uCKgxtswiobXnIIVzEjJ+Dt5zosrONC1R0F1bMO6HJZeqS2XNJd7T80iTW12t ys3zr8LtYO5cSUXyJkpxxzSZv+FfoSU/B7vSuWcLDR2iX9jZbmxiRGy8U26xe39UMm5yEpFr i1fktnKqH8N0xjT5tKZRfRg40es3yuE2QPL6uxcP0w4ia7WJ4Qiz7MwjJYfrFrPEyzslEj2k aObcFgv9/as6+T6ebXmuoGTN5VphAH/M6UhhNSyDfg+PwMTRWaU4/6826fm/UDhQLVFkPk2k q7BvZDfP8sbp6q5DxZb04Ym9hqzFjmm3dQFkXUdI1JFfxWHj4ftO17QOvz3EfC/g1G0nDdqw fDJIKHhD43TInTflLrtZ7Vw5k5GxAYu09xS5IhYB7EcLP7rX0/+rt3YDhs3MwyuxObnDc1w2 ZkFVmKPA6+ZK6PSvkGL5u41OeaMYpUauDDgJPQ/5v7ujGM5mVAGcKmm2JsYcnG4HvB8L0qFZ nrsh88NEWERsQUmVuzllEWCUSJPZ3a1R68w+yk3CJi6AofbWoCtnLuB0T+nEZ1Rf2BKE0yDE XP1d4qfQPoMcyKTIsp5kjMeT7ShSokh1QuvtADg0bZnIPDUqWUkssfo08Ew7OnOn1lm/jttS s+ZzmulTmdun2pOSSVgj45lpkko412D0LN4jv8QPNpa4f8BBg4wNZ/Hz+F5Tdn0UwTNONaIV FmOTdCvADV3RdU0lYxdK31hEsmv20iQlxGhBKUYwuTj7P0c96vd2yK0PMNh0zPc06JniVA6Q 8xJPGngh6hl9gGVCZSa216BmfOMcqIRlDXI6H/F1XCH6UhSUA9rUajGG3kZb03a69X4+kzqQ LqnCLBhOQxEmoaZMqUfUtTylh1dQev7ftHXYma/gWC1UB+CxrKXbIfpPWwb1SPRTkkFjw878 nOPNAx4DSCk8CrFFDI7M1Xpbgv39PVm7nO2Skhh1waRc0hozKa44DYQjP2YDuwWh/cK5X5np DJzE1KwmdnRDrJsviJHe6NRKZM46VZDjyfCshBle4anJOZkj0IfdAJ+uwXv0Q92A8NOi5piq nRi1wd0Ja+CtTEJPzqFwZD9PKHWIWju7ViubaDRwFTXzNeR/O8G9v05r1zpuAzhGFAl9j1r1 Nxc0n3U4ZuvbkJaWJjxU103+hs8rrfTZCV75oLI2lVjNKC1tnnJ3NdoTOopxxC8fstOZbueH VyXcYVSDMyvJeo23lmxO0hcbaYCqehtZZPgKqLVvczjdPxtlz+nk2ldtYV000bWsjF5VvaNx ZEOhfeRwgqAUT74ylanqMH+345eNlRwViKyzzbpAIlJa+h8Z4EOXC2nKc223dVzhNjkXXde+ BiiBk8J8MCscBuWKVf62EcDsCZf6Wzigia+wzFuxnsgpKqexyzDwKLrchMBNihKRXVtpVjpK ImwydsdWQL7Cmph3Avg7kH8ya9Boa15JGSGWkZEcR/9KGR6W7exvL6PCyJWwKshqj4fEOG1Y FTAD6X4vwNfySToWW1X2DE8cTiu/JT/hR1zzmyHfj5/q3/QeMc4whm6hpSUTPRR3yEGSSo+g D/eAFT6Pti18v2bkp7Ctqa1UGfpWpBIcCbtxJ+Nr2PhvTwsUUD5xqrj3IC+WQEhtE2zn8FnT yDJsArxbsHw2qK2PPgmNkhkCVng6tZrT4R3k48+npYVijARgpSY+2ZCkH+ma40Kn/KjKiNXF XhWmo2wgkCtwkBoI3OXypisU3ycxpEkfNymeiYM3Sl76clWCaCS5bgCnC1vo1P+oxiCBJo11 job1/Yq72YXxu8Tvw94hCyXArEJHURbeyXqnhKEqdG/sKp/a2OmcLz2301714PEbvnKskRHV XD1d413VyZ67sRkMF/PlnT144foPtjRcd07uRidkhOGhO9QYsFU9LJClW9sPmTzumcgwugwg El13J20i4OALn1k4KOzBhMLfi2wfc4Y/SvhyLpPhsvDlZ76BY1vQ39YOfmgBeLtCj8Zsu7rc hqDACFp4GnOAqLRREee8Bs09C+JSsHzcSvLez9Bio8+DBiFeB4B3EZOB258x8BhUFjtnZ2EE g8x5yhNtACm7EIUkKQwcUG4CD+XpR/0OGlqDsLDfVwGtkcaoB2Nec2GsrAsRWcBotv4/VbLc ivCN2EqRSkIQhDWWAylZ+Pzo4GGq6/BWKK/N6ecOO3e77UBCLHYg8roiNIu/i7QZJzQZT87X qF9ggwbGiknfqaR0zQXF35Nz3OLP5Pd/U3svHUw95/38ey3Cli2u83SW/0LYI8po1fv0O+CL 7LC3n8nb2wDh9VXnzmQj+FOuTxawzdncz3neVgZnQjKSq+Y2qpeDhpBLjh2KNMN9aU3mA9EJ c/cjNrxkL9+lP88TVlfBxTnnYmyaMoGLnvYVhuPDVuXNLmAOTzAwt3mKaK6R7pKiexIthq28 T+FGk7nNz6HmnHnTReqee1LiSiaOlRZtuTfOl51DnP/Sdv9dhChGNp+jDlz3rhtw32XbCgTN j9zd04LpbqVrGtZjvh5B21d/y9lIO2DyEP7p6HTLpcbt+cuAzwhzboLpiRnjeIPvGcZHa8Q+ mOatNNlrlC4n/PazzNmVEALsTNXnMeRuk4kP6zF955GUHKC/RQX7GzWBQ5ZwrktQtDppa1Uz cDC0azpLzIXudve/coHB8XXbsuBOXwtdxvoBDH8Aw4MTDrtPmbazR848rna5jiOo542p4K50 oIJUaNeXUcpG+kyD01kGJkdJc4yUG5917Gci8EM6Dy1qxybF6A49tjXE/mVB/voMjOQi7JJM gAJzb3PJoMWLoTn2kZmZzGSeazFHkPRWZZGpSgzNmfcQW1I+Xl6C3I2ggfrN1rr73gUGvq52 BUxj1kmCQzC3Djp6lYzYFHNoXlp+HQ=
  • Ironport-sdr: 656959c0_tRBZKglZlaI1+bQ2cRNGqWlklh3w1bqgMK9/wKUmFVtxyjM OVYps/v3HlDz/ARkWRtxx7mqUOG4ATXO77XHJvA==

Is there a way (e.g. optional flag) to get Print to print fully qualified names of items in the body?

Require Import QArith.

Definition xx := Qmult.

Set Printing All.
Print xx.
(*
xx = Qmult
     : forall (_ : Q) (_ : Q), Q
 *)




  • [Coq-Club] fully qualified names in Print, Abhishek Anand, 12/01/2023

Archive powered by MHonArc 2.6.19+.

Top of Page