Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Ltac versus Ltac2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac versus Ltac2


Chronological Thread 
  • From: Jason Hu <fdhzs2010 AT hotmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Ltac versus Ltac2
  • Date: Mon, 30 May 2022 15:38:31 +0000
  • Accept-language: en-CA, en-US
  • 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=arcselector9901; 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=+YoZqt79hzT09Ii9do3wVDfsGmLPR8lQNGc0OqUcVuc=; b=nUHt1fIsxREjAtTONeFx+1Cx+E8m2J3z8SGcAMAuFATvXGHlj/MjBW9QCGCUymFqqpsdU8Hp90MinEmTFOye7tUZp0xcg1p6FWOqnP8VgQ2gqe0L0zidm2zzw7l1Au8fLmSmH6zXILTKwebsf259yZ95LlQOPvf3gS0ejpS8CNzPEpmFqjOxDsnfOySnH7GaBpwUKYBoG6mlAL9I85O1Wc/xZ8gh9W1FG5cBc5caFLpwgjhNvoYD2CPqQeH0TUJJEOVuvBScSoj3844/KXijBBzNd+80F0fRHDXE3ye6KxzWhoS9F20aysJaqH7LHD1VvELye19zZA9bflkglBhz6g==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=U4UFALvcEH37Iop/+yS6bZ9JUUz8L7C+Duevkrguvz7nmcgiWXOuK40RHTC2GL/Fc3LxN9USICr1AIpR0Ntcq9pyNooXvQiJiUCDAwQ2f6qJHSyxuIpCFBTp63h0/WS3n9hXIgvzdV/AP9MT7Ir+YWwbNxXXiGn+7GVSmVfsRBwCVIDI3qKEL6ee4AOdNYgs+CjfHd/AUwPKiMBr4oGo0X0M6gEN+9L0aWa044478+5IhcJthp0hne8bEAD2VjCFpyLoxM1g+CPQdva0wmQ5U61DQLdNy9bI1FtedI5Ey2NWJwr2ozqQ99N/GWA8ATS6hNsO7bkUXR+S38m3hN/R7Q==
  • 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-DM6-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:8XIQEa6dWic5sdlX17AXZgxRtEHCchMFZxGqfqrLsTDasY5as4F+v jZLC2+EOa6NYmvzfYp1Ot7l9UpVu5DTzt9iTQc/+SEwZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UoYoAwgpLeNeYH5JZSlLxqho2+aEvfDjW1nX4 Y6p+5WFULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 IRysaKQEioQBZKPs7kGXwYINwtfD4QTrdcrIVDn2SCS52vvViK0htlLUgQxN4Be/ftrC2ZT8 /BeMCoKch2Im+OxxvS8V/VogcMgasLsOevzuFk8lXeIV7B6GNaaG/WiCdxwhF/cguhAEfbMf JBBMGJHbBPcZhROPhEcD5dWcOKA3ySjKWQA+AL9Sawf7jDxwh0s6eHXIvGLWPPTRNhSnGTEj zeTl4j+KkpDb4fAodafyVqngfaKlifmUqoJBbig/7hrhkeSzyodEnUruUCTpPC4jguyXoxZI klNoi0qrq5orRT7CN7gQxe/vXiI+AYGXMZdGPE77wfLzbfI5wGeBS4PSTsphMEaWNEeFAMu6 H/SsurSOn9E7aaZViK53JamhGbnUcQKFlMqaSgBRAoDxtDspoAvkx7CJuqP9obl0rUZ/hmgn Fi3QDgCa6Y70ZdVj//ilbzTq3f9/caQFFVdChD/BDrN0+9vWGKyi2VEA3D34O0ICYGYSFSa1 JTvs5XGt7hRZX1heTzkfQngNLSg5vLAPDiCh1dqRsEm8zeroSf7LcZX/S10I1pvPoAcYzj1b UTPuARXophOIH+taqwxaIW0YyjL8UQCPYq0Phw3RoMSCnSUSONh1H02DaJ39zy3+HXAaYllZ f+mnT+EVB7285hPwjusXPs62rQ23C04zm67bcmlkk/3jevGPiDKFe9t3L6yggYRvP3sTOL9o 4Y3Cid2404BOAEDSnWKqt9LdQBSRZTFLcqs9pAIKoZv3TaK6El6UqSKntvNiqRgnq9PkfzP8 G31UUhC0F3ljGHGLgPiV5yQQOKHYHqLllpiZXZEFQ/whRALON/zhI9CKcdfVeR5pYRLkK4lJ 9FYKp7oKqkeGlzvpW5BBbGj99YKXErw2mqz09+NO2VXk2hIHFCSpbcJv2LHqEEzM8ZAnZJg/ uT9jms2g/MrHmxfMSofU9r3p3vZgJTXsL0as5LgLoYBdUPy3pJtLiCt3PY7L9tVcEfDwSef3 geSRxwfoLCV8YMy9dDIg4GCrpuoQ7EhTxIATzGD4ObkLzTe80qi3ZREDrSFcDXbY3z5pfe5b uJPwvCibPAKxQ4Ys4d1H7tx47g54t/j++1Twgh+RSyZb1O3D7phJj+N2swW7v9BwbpQuA2XX EOT+4kAZuTRYpO9SFNIfVgrdOWO0/0QiwL+1/VtLRWo/jJz8ZqGTV5WYUuBhSlbG6R4bdE+y uA7tc9ItwGyh0Z4MtuCiSwIpW2AImZcDvcBn7RDWMrHr1RuzVtPJ5vBFiXx/ZeDLc1WNVUnK SOVg6yEgKlAwk3FcDw4En2UhbhRgpEHuRZryl4eJgvWxYOV3KNvhBABoy4qSgl1zwlc170hN 2VuMXpzL/rc8jptgv9FQG3xSRpKAweU+xCqxlZVxnfVSVKkCj7EIGEnZL3f+UkY9ydQe2Zd9 bTBkGHhUjCwJZmhmCwvRURitvrvC8Rr8RHPk9ymGMLDGIQmZT3igemlYm9R80nrBsY4hUvmo +h2/bkvNvSrb3JI+6BrWZOH0bkwSQyfIDMQTPxk+pQPFz6OdTy33w+INE3sKNhGIObH8BPjB sFjTi6Vu89SCMpaQvEn6a8wz3tcutcMvYJHVpa1YGkMvv2YsyZjt4/W+m7mnmg3Tt5ykME7b ITMazaFFW/WjnxR84MIhNcRIXK2OLHoeyWltN1ZMs1Qf37AjA2oWUE1zr69vnHTOwxil/5Rl B2WfLfYloSO1qw197YB0cx/68GcKdTvUe2J9Ea4tNEmgRYj9yvRn1t9l2QL9Di68VfctxqbW FhNXBPKMJv5gYsL
  • Ironport-hdrordr: A9a23:7AHDLKCrxuTaX+3lHeh0sceALOsnbusQ8zAXPh9KJCC9I/bzqy nxpp8mPEfP+VAssQIb6Km90ci7MAbhHPtOjbX5Uo3SODUO1FHIEGgA1/qX/9SDIVyYygc178 4JHMZD4bbLfDtHZLPBkWyF+qEbsbu6Gc6T5dv2/jNId0VHeqtg5wB2BkKwCUttXjRLApI/Cd 61+tdHjyDIQwVgUu2LQl0+G8TTrdzCk5zrJTQcAQQ81QWIhTS0rJbnDhmj2AsEWT8n+8ZqzY GFqX2z2k3v28vLgiM05VWjoqi+q+GRhuerMfb8wPT8cl3X+0mVjcpaKvO/VXsO0ZmSAR4R4a LxSlEbTrNOA3+9RBDOnfLB4XiQ7N8V0Q6T9XaIxX/45cDpTjMzDMRMwYpfbxvC8kIl+NVxyr hC0W6Vv4deSUqoplWO2/HYExVx0kakq3srluAey3RZTIsFcbdU6YgS5llcHpsMFD/zrIonDO 5tBsfB4+s+SyLoU5n0hBgR/DX3ZAVOIv6veDl9hiS0uwIm4UxE8w==
  • Ironport-phdr: A9a23:KojzRRbkNMMdtYdS4oNWWCL/LTEt2IqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gSPDduQu60MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9LiTe8br9/L xe7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+T bxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspQjmp8 btlRwH0hycGLz458X/YispsjKJAvRmtowVzz5PIbI2JMfZzeKTSc84HRWpaRsZeSTBOAp+yY YsICuoOJ+dYr4/grFcKohazAQygCeXoxTFVnn/5x6g63P8mEQHaxQAtA90DvGnWodnsKKseT P2+wK3GwDnfc/9a3DHw5orSfRAko/+DQ6h/ftfPxkk1Fw3Fj0ufqYj4MDiI1OoCrXKU4Pd+W uK1lmUpth1+oj+1xsctjInJiZ8exlTd+Slk3Io5INu1Q1N5b9G5CptdryGUOZVrTMM+TW9mu zo1xbIdtJGhYCQG1I4qywLDZ/CadYWD/xLtVPyWITd9nH9rfKiwhw218Uim1+byVNS020tNo ypLj9bMtnEM1wfN5sSbV/dx4lys2TaI1wDP7+FLO0E0la7BJ5E9xb4wk4MevELeFSD5hEv4l rWZdlk4+ue28eTnZK3rq5uAOoJ3lwzzPbkilMOxD+gkPQUDXmqW9OSg2bH+4EH3T7RHg/k5n KXErZzXJcAWq6y4DgJW3Ysu6hixAyq63dkegHIJIlVFeBedgIjoPVHDOP/4Dfajg1SsjTdk3 OrKPrzmApjLM3PNk6/hcK5y5kJA0gY+yc5T64hbB70cOv7/R1P9ud/AAhMnMgG43+jqBdBg2 o8CQm2CA6qUPaPPvVOU4+8jPuaBa5MQtTv4KfUo4ePlg2Ujll8HZ6ap2IMaaHCmEfRiJEWUe WLij8sGH2sXogYyVeLkhlqDXDJKYHa9RLwz6is8CIK7EYfMXYetgKGH3CimBJFWfnpGCleQE Xj2a4qER/YMaCWUIsN7lTwESKShS4sm1RGptw/20aZoLu3R+iEAtJLj0sZ65/HLmBw96TB4F cCQ33+XQ2x7g28EXSI60Lx8rEBlz1eMy6l4g/hWFdxJ4PNJVx83NZDBwOx6CtHyQRzNcsuUR Fq6WdimATYxTs40w9AUYkZ9H8+ugQzE3yqvG7MVkaeEC4Qu8q3Ax3jxO9p9y3He2aU8l1UmW NdANXW6hq5j8AjeH5LGk0KAl6qzaasc2DPN+3yYwGqVvEBYVRZwXr/fUXAeYEvWt9X56VnYQ 7+gE7R0ejdGnOWFM+NhbsDjxQFNQ+6mM9DDaUqwnX2xDFCG3OXfQpDtfjA/1T7aDgAkjkhH8 3qGJxNkXn75i2LZEDlnFFapaETpp7ot4EinR1M5mljZJ3Zq0KC4r0RO1JR0KtsW17MA42I6r ilsWU26x5TQAsaBoAxoeONdZ8k86RFJzzGRrBRza7qnKa0qnVsCa0JvpUq72Rl3GJ4ayZFyh HMt0A97KKbe21REJHuDxZ6lArTMMSHp+Qy3Lavf21XQytGTr6kD6OYj8Q265CmpEVYn+nRjl dJS1ijU/Y3EWTIbSom5SUMr7156qrXdNzE6/J/R3GZwPLOclBbngopsKM57jxGqcpFYLb+OE xL0H4sCHc+yJec2ml+vKBUZIORV861yNMSjHxef8IisOuso3DevjGAcpZt4zlrJ7C1kDOjBw 5cCxficmAqBTTb1ylm74IjxnshfaDceE3Daq2CsDZNNZqB0YYcACHu/a8yxyNJkgpfxWnlev Fe9DlIC0cWtdFKcdVv4lQFX0E0WpzSgl07ah3R6nzE7tfDHhXTmw+P+cRMGPihAQ2wjxVbgL I6ojswLCVCyZlthnx+k6EDmgqlD8fgnaTiJBxsROXGufzIHMOP4rLeJbs9R5Yl9tCxWVL/5e lWGUvvmpANc1Sr/HmxYzTR9djewu5y/kQYp7QDVZHt1snfdftl9gBnF49mJD/Bd3igdHnEh0 RHXAUS5Ntitu96Tkt2Q14L2H3LkTZBVfSTxmMmOuCup/jcyWEWXn/evn9TmFU4x1iqxhLwIH W3Y6R37ZIfszaGzN+lqK1JpCFHL4M1/Aohik4E0ifn8wFAij46OtToCmGb3apBA3L7mKWEKX XgNysLU5w7s3AtiKGiIzsT3TCfVzsxkbti8KmQYv0B1p85GCLWPtuQdxQN1pUa9pAPVJ/N6m 38RxOAv53gTn+wS8FZ1iHTHROxLWxAAbWTljFyQ4sq7rblLaWrKE/D4z0d4kd27TfmDrgxaR Hfla8InFC504N94NQGE23ny54f4PdjIOI5L8EzO1UuZybENeMFU9LJCnydsNGPjsGdwzuc6i UcrxpSmpM2cLH0r+qulAxlePzmzZsUJ+zirg7wN+6Tel42pAJhlHS0GGZXySvf9Wjweteb8b V7XSBU8rWueELvbWwSY7Q01yhCHW4DuLHyRKHQDmJ9sSBmPPxYH2Vg8XDImm5c4Ekahw8mrI yIbrngBo1X/rBVL0OdhMRLyB3zeqAmfYTAxUJGDLRBS41IK9wLPPMeZ9O42AzBA88jrslmWM mLCLVctbylBSgmeClvkJLXr+dTQ773SGL+lN/WXKbSW9b4CD7HZn9T3lNMhpmvEN93TbCU6S aRjhQwbGyg+Qpq8+X1HSjRLxX+XKZfD/FHkvHUw95z38ey3Clu3uc3TVP0Kd40ook/+gL/dZ bSZ3H8rcG8BhJ1QnSeamv9DjDtww2lvb2f/S71Y7HyUFfuClPMPVExJLH8jfMpO5KYh0gQfI tbVhpXtzLlkg/UpClBDE1v8hsWuYs9MKGa4UTGPTAOCMLDMTdHS6/n+erj0CbhZjeEP8ga1p S7eCEj7eDKKizjuURmrd+BKliCSehJE6smxdRNkCG6rS9yDCFXzKNhskTg/2qE5nFvsHEtFa X1QVh0IqbedqyRFnv94BmpNqGJ/KvWJkDqY6O+eLYsKtfxsAWJ/kOc/gjxyx7ZO7S5CTeB4g 2OO9pg/+Rf6y6/WkmovWQEGsjtRgYOXoUhucb7U8JVNQzeM/R4A63mRFwVfp9ZhDY6K2egYw dzOmaTvbTZapo6Mu5pGQZSNbpvfYClEU1KhAjPfAQobQCT+MGjegxcYi/SO7jiOqYB8rJHwm Z0IQ7sdVVovF/pcBF42eb5KaJpxQD4glqaWycAS4n/r5hfdRNdB5MieDtqSBunqITedy7JDY lFbpNGwZZRWLYD910F4PxNim5/WHkPLQd1XigtIS1Zs5Wlorj15RGB13F/5YASw5nNVDeSzg hM9lgp5Z6Iq6Svo5FA0YFHNoWFj9St50cWgijeXfjnrKa62VowDECv4uX86NZbjShp0Zwm/z gR0cS3JTLVLg/58ZHhm3UXC7IBXF6cWHsgmKFcAgOuabPIy3RFApzW7kAVZsPDdB8IqlRN2I 8L06SManVolNJlseOTRPPYbkgAW3/rR+Hfujqdonmp8bw4M6D/AJXRO4RRQcOFgf23xoqRt8 VDQwmMfPjRTEaJs+rUzqQs8I7rSlSu4iuwacxnjObDHd/HL/DSQ8KzAClIoiBFSnhEcr+Evi JUtLxLPBRJokOvZFhICMdfOJFNOd8ResmDJejqDuvnMxpQzOJihEufvTqmFs6Nx4ArsWQ8tG 85kBiUpOLCJiRmdAeK5abkPxFMq+RjhI0iDALJRYhWXnTwbosa5iphqwY1aITJbCmJ4Y3zfD lP/pgg2hfOCWJE9ZXJIBuPs2Vo2X9G/ki9d+X9HCWvuut8=
  • Ironport-sdr: 6rUSfu4olMog9iHoOajUjFlpIBVM/rAJmtLpkZj+1iO1V1xJqJ2F1iLOM68KX0+tXXyJb5dr0v FtR9OUnm0zNYLOw+ZgWuUdvQYy/DDlDig/1xxTyDkRDICga5XDqEpikaiwd4mSrJ0bnkS0yznH yNoL2PqqQyfUe0rTmJIQbu7aUNif5dbIaJ5aA2QEqffnHlhl7K9v0vLobzaOEFzBW7dSnxUpFn wAJowC4YOFb6bSVsLrxqA2FTrgrjd0hbZZ+tNQv/vkOHTlxOfQbn1ZfAA+K1+wedKUASOSuPnv RoNl69X9GIAzI7c1LJUkCNE/
  • Msip_labels:

Hi all,

recently I am looking into Ltac2. I know Ltac2 has been around for quite a while but I have not heard of much discussion about it. I guess one thing that usually comes up is when there are two choices, people (like me) have hard time concluding a final choice. Moreover, materials out there for Ltac2 do not seem as abundant as those for Ltac.

I once used Ltac quite a lot. What is the current status of Ltac2 and why one would move to Ltac2?




Archive powered by MHonArc 2.6.19+.

Top of Page