coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Hu <fdhzs2010 AT hotmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] update a tactic
- Date: Mon, 23 Dec 2024 05:18:14 +0000
- Accept-language: en-US, en-CA
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=1VjmMOdtdbenxXTurzRKSDmDUBI6NQOuJn9o4FdLGSA=; b=U9AJGVAD8pQch+xuvjCFHUJkGYlFytYDHwWEK01E1KDzR49DBp2Q1XE8utTkktBlRAqT9j6gcyoPg0tkd+8Dt05+1/R1Ah89wBDfgSQMU5APotZENHQ/rYVt6xglncZQ+hD+HHBA1GwC690xTBG2MxcIAUJtETRdR0GLoggVqrQ4FfYXbg8cDbXApyi6bOWP+1fL53AmlT6SubBKsoM+0dCDfmoxsvima2gYkzF+xXalk/VkIyJRnYPFLWxMVVRfGhjtrGxlsPA+okZ2WBD+SUYyf0EICstFCxcUZp0RbnAFn9yhkLjYe3zn6MzqAsUEWnsUE/kEHE1cShbe/pJzGw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=uqN6tNzBN72EFeOwjCPeqRa8imL7c3GHAyC6s68AlmRe9tcRJ+dzW2LRoBwz6enIqztJczCnuHMNtDd5DuG9Q8AdCIwZ9JUQJ8wVDOoI1EaCEJtA6rSs+chiTKELvzAFxnhGpapqQXzEyGwPR1TTw/oCxvoq3k+UkSKt++R/NJPx9FRXstYbEx6jIIj1mRJnC+gYngn7StomQtkEa79VbMah3BUeZtKB8xvHNbptpD7UDPT1CmM07L/tzP04Mw93S0yJw8g7gLll7pW0fDPqBdOUHSlAtDFhbAgj7qOQSdnszhzl7w0xQC+pOlu9NbXvH2xZ7SEJdSfQZTxyldP/ow==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM10-BN7-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:SYCYi64ut8vBH4iTqKBIBwxRtA3MchMFZxGqfqrLsTDasY5as4F+v msdCmmFaaneZjSmfdwnaY+/8R4EsZ7cn95jTgY6pX8yZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgtaAr414rZ8Ekz5a6o4mtC1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6+QpLx4QAo8pw6FuUWNn2 +cpJWEgSh/W0opawJrjIgVtruIKCZCzeak55TRnxzyfCus6S5feRamM/cVfwDo7msFJG7DZe tYdbj1sKh/HZnWjOH9LUNRvxqH03j+gKlW0q3rNzUYzy2bfzB5qiuC0aPLVfcCPTMRR2E2fo woq+kygWk1LZYXGlGDtHnSEtLLIuQSkaoYoO7yS6vpWnQ28m2EpIUhDPbe8iaLi0BLhMz5FE GQf/TNrpqwv/mSwX9zlVlu5pmSFt1gSQbJt//YS7QiMzu/e5VmfD21dFjlFa9p87JBvAzs3y lWOgtXlQyR1t6GYQm6c8bHSqi6uPS8SLikJYipsoRY5D8fLscYQ0TTwTOdaV7fljPTbAgD9k h2uo31r71kMtvIj26K+9FHBpjujoJnVUwI4jjk7uEr1sGuVg6b1NuSVBUjn0BpWEGqOorC8U JUsnsGf6KUEC86LnSnUGOIJH7fzv6ncdjrBnVRoAp8tsSy3/GKudpxR5zc4I1p1NsEDenniZ 0q7VeJtCH17YSfCgUxfOt/Z5yEWIU7IToSNuhf8MoMmX3SJXFXblByCnGbJt4wXrGAikLskJ bCQetu2AHARBMxPlWXtG7dMi+R3nXlgnws/oKwXKTz3jtJyg1bFGN843KemMLFgsMtoXS2Jr YkCb5fUl32zrsWiO3WKrNF7wa82wYgTXsus95M/mh+rJwttAmY6DPHNibgmYZQNokimvragw 51JYWcBkACXrSSfd22iMyk/AJuxB8oXhSxgZ0QEYw33s0XPlK71vc/zgbNsJeF/rISODJdcE 5E4Ril3Kq0VEWuXq2xFN8mVQU4LXE3DuD9i9hGNOFAXF6OMjSSTkjM9VlK3qXlcPTn9rsYkv byr2yXSRJdJFUwoD9/bZLjrhxm9tGQU0rA6FUbZAMhhSGO1+qhTKgv1kqAWJeMIIk793Te07 VudLioZgujvmLUL1uf1q5qKlbr0LNsmLHFmRzHayZ2UKRjl+nGSxN4cceSQIhHYemDG2ISjQ uR3yPunCuE2o1JRl49aDbxQ7Lkf4uH3rORw1TVUH3TsbnWqBIh/I3KA49J9i61VypJduiq0Q kip+NJKHZmoYeTOD0w0CDc+S+aIxMEvhTjZ6MoqLHXA5CNY+KSNVWNQNUKujBNxAaRUMoQ35 /UIo+8TthKCjyQ1Pua8jix783qGKloCWf4FsrAYGIratRo5+GpdYJDzCj7E37/XUo9ianIVG z6zgLbOo59+xUCYKno6KiXr7Npn3J8LvEhH8U8GK1G3geH6v/4Q3iBK0DEJXw9QnwRm0eVyB zBRDHdLB56yphVmuMsSeFqXOVBlJAaY8UnP2Vc2hDXnb023ZFfsckw5G8iwpX48zUwNXwJm7 Im5yXnkWwnEZMve/DU/cm87pu3BTe5ezBzjmsemI8erObwGSCbcgfP1QVVZqincXN09tHfGr 7JU4dRbNLLwMH9IkZIdU4ClhKk0TUHdKENSX/s75744RzDAWTCt2AqhL1K6VdNNKsfrr265K Z1KDeBeWyuu0B2hqmggOpcNBLtvjdgV68EnaJqyAUIn756OsWBPor/L0yr12V8QXNRllPgiJ rPrdz6tFnKagV1WkTTvqPZoF3WZY94WQh/Vx8Gwrfs0EqwcvNFWcU0d1qW+u1OXOlBF+zOWp AbyWL/E/dd9yIhDn5reLYsbPl+acejMbeWv9By/l/9sbtmVaMfHiF4zm2ndZg9TOeMcZsRzm bGzq+XI5ULivostcmXnipKERrho58KzYbJtCfjJDkJmxAmMZMy9xCE42TGcCYdIm9Zj9MWYV 1OGSM+vR+U0BfZZ5lNoMhZ7LThMKp7ZTKnaoQGFk8+tETkYiAzOE8Om/yTmbEZdbS45BKf9A Q7V5der5s5Ug91MDSAbGsA8UoNZIUDia4QiZdbepTmVNUj2o1Kg65/Jtwss1iHPMVaASP3F2 JPiQgOkUgafo4TK8Y19n6ltmCYIHVBvo+UUVWAMye5c0jyVIjYPErUADM8gFJpRrB3X6Lj5Q zPoN04JFiT3WGV/QyXWudjMcF+WOb0TB43fODcswkKzbhW2DqOmBJ9K1H9pw1VySwvZ4NCXE /Ms0VyuAUHp2bBsf/gZ2dKji+Q+xv/6+GMByXqgr+PMWSQhEZc4/10/OjFSVB73MdDHz2TKA mkXeVpqYm+GTWzJLMIxXEINRT84umrjwQx9OG3LiJzatp6AxeJN9OznNquhmvcfZcANP/gVS WmxW2KJ5HuM12cOvbcy/egkmrJwFenBC/3SwHUPnuHOt/3YBqUb08I+ce4naugHoVYaOXWC0 z6m7j45GViPL11X1PuO0wIV9pltU3UKSTbUkAr4ojyAmhs8pzQcUwb/1xr1cPkctIC613i0g h9LBKpSn7FSnDvjuTx3t/BdrVuCaS3UPWeRSTgmF/sejT/1IFKw19ldP4US19VN9XRFwsNfc 6P5PxDRPm64dnvn4j0IV+v1rlSqQ3nt1+jDZ3LUEMpXK+aN
- Ironport-hdrordr: A9a23:BWpohq8q7AnaFnfSpY5uk+EAdb1zdoMgy1knxilNoENuH/Bwxv rFoB1E73TJYW4qKRcdcKO7SdC9qBLnhOtICOwqUYtKMzOW3FdAQLsC0WKA+UyVJ8SdzJ876U 4IScEXZ7PN5DNB/KXHCXyDYrMdKa68gcKVbInlr0tFfEVPUeVN/g15AgGUHgldXw9dH6c0E5 Ka+45uuyegUW5/VLXMOlA1G8z44/HbnpPvZhALQzQ97hOVsD+u4LnmVzCFwxYlVS9Vy7tKyx mNr+W53NTpjxn3oiWsn1M73a4m1ecJ+eEzSPBkv/JlYAkF0m6TFctcsvO5zX4ISaqUmS4XeZ H30mwd1oJImgTslm3Zm2qW5+DM6kde15bZ8y7pvVLz5cjiAD4qActIgoxUNhPf9ko7pdl5lK ZGxXiQuZZbBQ7J2H2V3am7azh60k6v5XYym+8aiHJSFYMYdb9KtIQauEdYCo0JEi724J0uVO NuEMbf7vBLdk7yVQGrgoFFqObcI0jbMi32PHTq4PblrwS+tEoJsHcl+A==
- Ironport-phdr: A9a23:fHidhhwgwfIL4wrXCzJhwlBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xWZvK08xwCZFazgqNt6yMPu8JrcEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/9pPObwlSmTaxfbd/I Bq0oAjSq8IbnZZsJqEtxxTGpXdFZ/5YyWR0K1yNgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7U LJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5 LplRRP0lCsKMSMy/XrJgcJskq1UvBOhpwR+w4HKZoGVKOF+db7Zcd8DWGZNQtpdWylHD4y7c oUPEvEBPf5GoIbhu1sAoxy+BQy2C+PuzD9Dm3v60KI+3ugkFwzNwQ4uEM8UsHnMrNv7KrocU fy7wqfL0TrMYOhb1i3h5ITUaB0tve2AUa92fMHMyUcvDQTFjlCIpILhJTyVzeMNs26G5ORiS OKklmkqqw9srTivx8YskZfFip4IxlzY7ih5wIE1JcG9SEFhYN6kFIFcuD2dN4tzW84vRXxjt ykmxLMco5G7YDQKx4o9xx7Zc/GKd5SF7xH+WeuePDt2i3xrdK6wihuz80WtyvHxWtSp3FhFr ydIltbCum0Q2xHT7sWKSPpw80Su1DuO2Q7f9/1JLEYpnqTVLJ4hx6Q/lpsVsUnbES/2mVn2j K+Ldko/4OSo6uPnb7P7rZGfL495kg7zPrg0lsG7H+g0KAcDU3SB9em+ybHv5VP1TbRWgvA4l 6TVrYzWKt8aq6O8GQBZzogu5hO/AjqnzNgVmHwKIE9FdR+BkoPkJVXOIO3jDfejnVusiiplx /HHP7L/GpjBMn7Om6r7c7ln8U5T0g8zwMhf551KDrEBJ+r+VFftudLfExM1LxW4zvv/Bth/z 48eXnmADbGDPKPVrF+I+vkgI+6RZI8TpTnxMeAl5+TpjX8lh1ASYbWp3ZoQaHC+BPhmJFiZY WbogtcGFmcKvRAyQ/DtiF2HSTJTZnCyULwg5jwjB4+qEZ3PS4SzjLCb0yq3Aodaa2JbBlyUF HfnbYSEW/MCaCKIJc9hlyQJVba8RI8h1BCurxH2x6Z6IubI4SAYtZXj1MRw5+LJlBEy8SZ4A Nia02GIV210mHgHSCcs3K9juUx91kuD0a9gjvBFDdBT/e9GUh8mNZ7AyOx3E8z9WgXYftuQV FmmRsimDioqQ9Iqw94OZl59FM+4ghDC2SqqGb4VmKaRCJw66KKPl0T2cu160j7t0LQrxw0tR dIKPmm7jIZ+8RLSDsjHiRPKubytcPE+1TXK8i+j0CLask1YQhUqCfyddXAYek7frNC/7UTHG ez9QY87OxdMnJbRYpBBbcfk2BAbHZ8LWfzbamO1wCKrAAqQg6iLdMzscnkc2yPUDA4FlRoS9 DCIL1t2HT+v9kTZCjEmDlfzewX06+Arpn+7XFRul1jSR01my7+8+xpTjvuZGLsIxrxRgC46s H1vGUqlmdffCt6OvQ1kKatQYcEmug8ejUrZsBB4N52kaatlgw1WaBx56nvnzA4/EYBciY4qo XctmRJ1Mr6d2Uhdeimw+7nVY+WSAE+tuRelZujRx03U18uQ9uEX8vMkpl7/vQavUE0/73Fg1 NoT2HyZjnnTJCwVV5+5EkM+9hwh4qrffjF4/ITMk3tlLaiztDbGndMvHuosjBi6LZ9ZN+ufG Qn+Htd/ZYDmIfE2m1WvchMPPfxDvK8yMcS8cvKa2amtdO9+lTOihG5D7chzyEWJvyZ7T+fJ2 d4CzZT6lkOJWzfulw3565jfmYdYYDgTGiy0zi2lTI9da6tufJoaXH+0Kp7/zdF/ipjxHn9Ao QL7QQJcnpPxP0XLPDmflUVK2E8aoGKqg369xj1wyHQyq7aHmTfJ26LkfQYGPWhCQC9ji03tK M66lYN/PgDgYg43mR+i/Uu/ybJcofE1IWXTU1wSJ3GuB2FlTq65t77EaMlKosBN020fQKGnb FaWR6So6RUW0zH4RTMHnBg7cC2vs5T92Rd9jSjOSRQ75GqccsZ2yxDF4dXaTvMExTsKSh5zj jzPD0S9Nd2klTmNv6/Kqfv2F2eoV5kINDLu0ZvFryyjo2tjHRy4mfm33NzhCwkzlyHhhZFmU iDBrRC0ZYeOtezyP+5nbFIyXAakw8p9BoR3k492j5YVkXQXnZSa+3MbnHy7bY0diPi4MCJLG mdDysWd+AX/3Ux/Mn+FouCxHm6QxMdsfZjyY28b3D4889EfDa6V6LJemi4m6lG8rA/Xfb18h mJBkb1/sjhG26dW4VlIrG3VGL0ZEEhGMDa5kh2J64v7t6BLfCO0dqD20kNinNenBbXEowdGW X+/dI1xeE04psh5Ll/I12X+r4/+f9yFJ9wftg+PyU+Z18BVL440n/sOwyFgPCiu2B9tg/5+l hFo0Zyg6cKJJ2V/5/jhW0ZwNjrpYsoS/nfmiqMUzaP0l8i/W55mHDsMRp7hS/mlRSkTufrQP AGLCDQgq32fFOmXDUqF5UxhtX6KD4GzOiTdOiwC1ds7Dkr4RgQXkEUOUT49hJJ8Cg262Jmrb hJi/j5Irl/g9kkRkKQxb0K5CiGH4173IjYsFMrGdEYQsl4EvwGNdpXBi4A7VyBAos/99Ercc CrDIVwPVD9BW1TYVQm7Yv/yup+aq67AQbDlZ/rWPefX8bAYC6jOnMr/lNMhpW3pVI3HP2E+X aRjhgwfAjYmRoKB3G9TAy0Py3CUN5Ld+Ej6p3Yx85j4qqijWRqxt9GGU+IAaIw2qR7q2f/RZ anM1EMbYX5Zzs1en3aQkepGhQdAhX02LGv/VuhR/S/VEvCKk/cOXUdCMnF9aJMTvfJkhlEfa 4mG0raXnvZ5lqBnUV4dDA64w5j7a5BSeDO2bAufVhTMae3OJCWVkZv+OfruEOQJ3usI70bit 27DSx2xeWnZ33zgUxTlWQ1VpBmSJwcW+IS0cxI2THPmUMqjcRqjdtl+kTwxx7QwwHLML28Vd zZmIQtBqbiZ7CUQhfsaeSQJ9n1+MeyNgDqU9cH+A7NP6b5BJHsxkOhXpnMn17FS8SdIAuRvn zffpcJvpFfglfSTzj1gU1xFrTMu5srDsUh5OKrf/4VNQj6YpFRctyPMU1JV/pNsEZX3trpVy 8TTma67MzpE/9/OvIMdC8XSNMObIS8hPB7uS1u2REMOST+mM32ahlQIzKnUpyfT8sB89cG// fhGAqVWX1E0CP4AX0FsHdhZZYxyQithirmDysgB+Xu5qhDVAsRcpJHOEPyIUpCNYH6Ui6dJY xwQzPb2N4MWY8f110xwcQMixdziG03MWNlMpmtqaQp+8yAvuDBuC3Y+3U7ocFbn+HgICfu9h QI7kCNYSMF0rHLGxQhyIVDH4iwtjEM2hNPpxyiLdyL8J7uxWocQDDfos082MdXwRAM/PmjQ1 QR0cTzDQbxWlb5pc2tm3RTdtZV4EvlZVaRYYRUUyKLfd7Ay3F9bsCni2V5f6L6PF855jAVzO 83JzToIy0d5YdUyP6CVOKdZ0g0amPeVpiHxnuEpnF1CfwBcqiXKPnZP4RFAN6F6dXbwuLU0t kra3WMEITZpNbJio+o2pB5nfb3Yl2S4leYEcx35NvTDff7D/TGYz4jQBAt3jx1AllEZr+Usl 557KAzMERholeT0dVxBNNKee1gNM4wOqz6LO37J6LqFwIorbd+0Trm6FLbX5qhI2hr2TkF1T +FupowABsf+ikiAdJW+dedXx0l1v1a5YwnURPVRJkDRmW9e8Zjmlc15gdEGdGFFWT0vY2Lqv 9O17kcrmKTRBt5uOyVDB9JWOC5uA5+xw3YB7SYHUWD/0/pHmlKLt2au/32JXjegN4Exaq/MP UE+T4zssXA296z84bY22rP3AjiicP5E5ZrI4+5coIubAfRJS7U7q13bh4RTW32tVSjIDMKxI J/zLYIraI6tYp5fely4lzc8TsO3N9GofPDgae7ARYFItYCa2HYoMsrvT1kj
- Ironport-sdr: 6768f29a_/Twqa0XtkyZZeucLvFbBqmuK3ALUlNkfX1W7EiZrRGBqwH9 gwj2yc0NxS5tlmKR+CrUQLCtYp290KjHfsJ1Lzg==
- Msip_labels:
Hi all,
Is there a way to update a tactic, so that it invokes the old version of itself?
Say,
Ltac foo arg := do something
Ltac foo arg ::= old_foo arg || try something else
I've tried a few things to fill in old_foo, but all ended up getting into an infinite loop.
I would like to update the tactic, instead of shadowing it, because I would also like to update the behaviors of other tactics that use foo.
- [Coq-Club] update a tactic, Jason Hu, 12/23/2024
- Re: [Coq-Club] update a tactic, Gaëtan Gilbert, 12/23/2024
- Re: [Coq-Club] update a tactic, Gaëtan Gilbert, 12/23/2024
- Re: [Coq-Club] update a tactic, Gaëtan Gilbert, 12/23/2024
Archive powered by MHonArc 2.6.19+.