coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2 retraction bug?

From: Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac2 retraction bug?
Date: Wed, 22 Apr 2020 23:03:17 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=s8mawutt AT stud.uni-saarland.de; spf=Pass smtp.mailfrom=s8mawutt AT stud.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Autocrypt: addr=s8mawutt AT stud.uni-saarland.de; keydata= mQINBFWVkZsBEADmp2Mq5XZcOg38F91SMR5uF8cqC7LaODrnF+xh3TNKgbK301sPwcSKA4gr +TKV73e4VQoWihiWaYfPJYHsudXrp644dqYvWuxNWlkh4S2HIOmcopuTEd063TL5hRvhkg0V ZOMq000ucKo0yBsUux7+TdZdDAX3WP1whF7jY8OTe5xnEO3yv4xydAZhbT/gMO/IW6BVE2xO eElXEwC8Tnssar8cM0wZcnxgKXq4dhjDO6sSkeaf81a6FPlpy+VuCIHFYoFIAquX6T6V+Zbi UXJyDSUSUVVmechLA8vXmiRgOTyVMdTejXQb5niLGjb/Upvy9uSlO7eR0aSkCs3vqeXIppmS PDTKVwPso/PmJHEJnZLrbXKqqh589pbDAdYfJvP3Sg0fncL5bzxV0gdSqWH0t0e7c9AMiHs5 5bxEHBXuVtNs1srF52gT0KlE84R2UOmZ9Kst7P3XgJtIGzuS5uSHqFmtknh9tj+/G/Kg3qDz njxM6xTGExNPHQuskwbvYDqA6/5Hslqis6D6EpMPGhRuUhPuE5Eb+PsxpV26UccZt51FqIIc Mwv+3AUPbF7v7s7rAE1BkbmClUGuYUGfqfndGT4V6fLpQH5F9kRdxmIm9FcMURUDvX4CBKZz gmwIZ4jgZ2jZ1VTy+MWIXRpgJIt5aim4liycyDoPk+fyYfdmQwARAQABtB1zOG1hd3V0dEBz dHVkLnVuaS1zYWFybGFuZC5kZYkCUAQTAQgAOwIbAQULCQgHAgYVCgkICwIEFgIDAQIeAQIX gBYhBD64TDV8welurJxMM+1Xu2bbvfzeBQJd7qlVAhkBAAoJEO1Xu2bbvfze9NkP92DvzDUh VM5IzQC+aK2M7Yo2NE5j3ELhZH1m+RZsU1Ek5evoBVX71WfIrBDHb92c5AUBPy3uzG9Rno2Y x6eE59BFr0CpGZ52G+JWjVxL2voBV8zuvI720lqHONv3zONK9OvaI0nE0XxV56NktzW6X018 8h4woo1amXu8jBxJcSdrwiS//T6ZqzrHAv00JWwmhbg57uwgvu07PcHDUSB93j8hx7RxP3UG bnTE1/3QRdwq4YDa/TO7v+EqEO8RCAlRtTCXnLlgRpIWPEx4+g4w9EGaBdc94YRgkEFh2U1z QuJt/3797P2iTiR3LqIXfSxTZUy/znMcy6q5Jl6A3+dms2JQRVjeA0yppajmxLDlz6zjZj91 BKIIXQbo5A8UiKDHWEgxq7Atyg/Bloc3njvaZ0+bGIKyciDT2Noyd8SHD4H390O/cD8LVjBt H6k/1wUFkX3h24dEFXASjA3vZCsmR/FI9wok9fyfpE/iqVXkUpmX20FNWJl9f9eLNSDKx7N7 foJSzwPVSGFSNhEY5BAjUkJrHOyHZ8tAShBJovxnIGfD2OtTqKLAEWHvm7+CYXeR91DjalPp /6iRd/xvRw6yisS+Nqi8X9gEBaq8vJemCV0psbU30brVs7dqKqaOf+N0PyCp/FDlCvYaAhEe kFgo4TeEqMe92xM49tzenY6I2vq5Ag0EVZWRmwEQALwwnvtVw/zFec+MNKgBwKt1MIG6EMBK c+OTIYM2tN4jcWlaAbEcIZGkBSeoPJeTi4m3GQXhifGZK29VoDIUQjYYDWNtp6U8y0hLRnqS VY/YvcTDnK929n5rqMqO0wYf1fzhmPshIyD1jj96tqu0ppX7zE++VQ/VJgVIA8IGcNXUN21A /+rJKCJFAvBp+6u2gNaUDfnqvPfTGtkq7A/D40Lo6y0KVu20R3W76iFWl6FEQzOe28VBnOjU /NbyzAzVUSgYCSfkYxhDiKfJRJvQd+VKUCAa+BSNoEPvDMKakvhApWUOncnNUbfXiH04fYSV iu2NH2Ls3HLm+6xaAaf9eUIU75A02xXUa6m+AccJQzCEJySeYJFVhJLSgZEbGwDZVdrRALol gYiIrwOHTitC2PLRej8HeywQrn3PUGBwiYdOa19KTHZykbO0s0SHb6bvm3vgpAPPdZp+QWPO Xx3aZz6dw4D867lisGVKMcKBcX9QCekVL7CW6lvvevUP5tBBYCshMvSTaN0BymBBwYrz8UB4 RYJ4cUs5apd1mMfD5Vm8EZf1DT15Q+K9+HsRQr3y/+AtHm0gd0DpXGfBH4H+54vyB9Aj3DVb yPMeFYv9UhyKALEomprFM0tr0+SPh275xXlIxUvoC+3PlFM0swoLSmi2Tu9edjU6GuyL91w/ 9WTjABEBAAGJBD4EGAEIAAkFglWVkZsCmwICKQkQ7Ve7Ztu9/N7BXaAEGQEIAAYFAlWVkZsA CgkQIA5mg0qOKkAoDhAAnms7o654V2uZWBsiiR2oEykGs/sIzxYcKrOi2RnkL6RAwhJgBr+W VpjQ2IS9IQ5Bxy8GOWhzyit2XvFYTWxGamrmyXol7IynGcl2U3WpmSQEPJx/QeyQ5lWLYzjn 5bbdzNdY0mhUnRZ+ke2tcttmvLsUKn2J/8lSyqBF4i4Yaj4p4LQ8n/K/eW9lIY+J/gVGDcrl ZqOozXV9aClYDtgxL/c6/TPuDi0vgkhIaojwsSu38YmhmbYP03ntiLTrLbjnJXr0pYIlMRqU mNvPsphOR8cVGFnZ50dVoWHSSJhoIESpu8Qz1qwvA9uNTDhe/nnr092diP78FWo4SENiKjrX A2fOjk0YoZA1uSL0RbcRKAttPC88iBWUyBwYrhMBFKzJeDG+lvBID8gED205Jy7Mk8v7R9Nq HpjJXST1avVMF7TXCH8OK7rgI9ATGLqJ31WoYZkCSFkYKYRbyarZnVKxMsQ1zhpjoEfuQlWa q2NgwS2cijWmKAmFV4Qv3FA5zAoEdzB9HCbT2DafITEUqjf111+WjNcfJvtfQcO7hghhMwFt W9Or9KqVKpEDrakuuHUr6nVnBNYCliY80m/X5DXOZsKzehxfHht4t+CydGE2xRzIwzpos2Ze bhkjWmghGS7G1JHADgEk7zBKyVxJm/nwwNGk5MdY9sckx8XMiaA5lV2oDw/+K7mXo2qbEPng hGjN2bAqYbZd/Wdh5SUwa5YvnfqWcSY7G8OA5pexnIV/5RRIdcc+RtrxADmfTYGVIvSfAS4u wALIgEd5LYdYBIajxWLCyNghoQowLqZbIQQ4eOWd2xCF6srcTsIou2kJ97iiFtXgX3PthKn+ fhdFYWktEDabDhgYSdqJVvs+Sk3lO41aJu5MSIsqWq+G0ZGumTtO/yR9x5RzA/qKn56S6Da8 WjRF6iq/oyemifyC74HXmmi6gd8HCWD+eEXNWVAVL/FlfYhL420olMcBgP+cMGJTpmWK5jCy axHH4RFYg8AAdzn0/Lc/Xr47IZBntCaLy3V1LSKvDSZackKOreBmxQrd2Qn5/seLYFWWl/rP vqib6hmoE17SjBI2szi/t37JGXTl0ZkhSUp6FSC4YmoFrKJgxuX0q7CONZzdZ9G7mNOkUdg3 QAaN6/EZQceGC/Dvi28jB57Y50OoOAcyJnSkS95lPobHcGbBDDIQVvcEBwhSir/coGXHk8tq MXCdhxDo9Tq1cSvANeRYuJdrTdJM2FMll7QEtBcto0DNCNEecvZ+D/uqOU+InyJHpD4qDpQR 8bqNJ3Fmehd54LYiZK2G5/gRwF+8vnaeoy9fSs/CAw3icKPTcSSmy9bOk3I0fgAyb63xLF/s GHAOq5gkPg+9o79dHcbtD425Ag0EVZWRmwEQAKYFa3Y6d5D34YkaNBYvjU3mUlaS2uq7khoV xhnPiad496PzpxpF76rwpAbh7+V+aqxFDldmydjV3REPgJKk5hnhJ2ndltaoy0CtzFOjUV2K kzzvG2YXADSKCqvLrtVx3wfAxOVxjPOlFzG57mvZd3MUlxOGJPvNbFJJY98OzjQGeCukITMO 4mivublSlJy8hNkwbMgkAfBkuITNXllrLfTxch6wikunYlDrtI2X1/h6ygXn/m8dYWzDGv80 PyzVHWNMz7JS5UuD7PkkazkqLzH9HQ+xj2x7KOWIHs9BQp99OrZfUMcD54EfoM0JUG5kq0Xs 099Z4UEFA2Pl+8mnn7z7NNZ1JSN0xjUuxhMu5deIkKEj8XGwB+6OXYEhF3mdh5T29C4LHDpp 3fpa9LU+8Dlpq0HJlwBx5ngXOfAmZrKAJhiy8kT3AfNskiVWxgYga2Kk2ku8vV4DkMai7kzK 45t0/cDwdgugeck83x/7yR9XIrBwlt8N4bdJ3URbOtnuGuYjM5RTtqpadjVLLr+ZdhKPdM7q tPfnHotjRq+ban1TdA/zlCOW+s4g955kvafY29qnhx54y+DQJUwELAZCTA0fT/eHs0n6M/gI LepMleBR7STA+XqnI5aWlWn3Pp6nI8t3bz0T6sFEocD++YJNEr/J7yduvcNaI84j03iRMfPj ABEBAAGJAh8EGAEIAAkFglWVkZsCmwwACgkQ7Ve7Ztu9/N4GJA//f21oF6/XClyTnbsNSBKL vbtb9CjKx+9c6B6k1qHePSylFf+BsrKFMEdtyn40bfVnQqQ1GzNFFbzGiFkUlwM1BZMR0ogl 6ahtJL3M4Tf7RkV6FUhkov5HwYIXDjx9WdboLPPz4NQkomgcWyc0vAndtL1vYFizVLkxIdWo nnv11M4MoQybCjv9lm+UwmoqLkSvrWn3F6RMPwsc4HWDRHiBYNkCxYGlfVfQax1u3ENH7KfE nZAEEoxSBkaha1Tv/06wHjQ9w+7ZwueiB48MCQleDM4xP+Geom/VIhExdySrAtGZEP7DjCpc XTYL6491G1gDdStpzSU0odKKxp3xUgB7gFuegBsM4dXm02Q6tzr+oVLkCeTGWld3/DfyIVVi 3f2w+g+JEE8W71GxuIw4IwuxXr0sGo1gHnH8CD5ky0/dGYfW644oZ6DQRzDqp+7sJNGoSOmE bJ5k7IgkPlwb41jNEz1miq/AIleDjVgM6ZP1g4eVAWgjATFqfv9y/WR1t1BvrcogGKdVLfRr 6kDYwP2GzzCGz2KiVtlPaPv52UYPa9zX6IT5hEOq4GSAVo2IHwtukyG10l7sanq7J6s5CumN ukDzuJxJ+EgNYIxaEtdujUPJxlRQcFwqjbLEt2LQBJivwzRhRmQfQz5tt3c797Tsto875TRg vFHu+ezStimb9ew=
Ironport-phdr: 9a23:PbfiQxX9153s01ccgYmZQSqBPBfV8LGtZVwlr6E/grcLSJyIuqrYYxyCt8tkgFKBZ4jH8fUM07OQ7/m9HzBfqs/a4TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrMYbjIltJqosxBbEpmZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJi3YDUboGbOvlwcKzTctwVR3ZOU91eVyBdGI6yaJcDAuQDMOtesoLzp0EOrRy7BQS0A+3g0DBJhn7z3a071+QhEBvJ3Ao9FN0OrXTUsMn1NKQMXuuoy6TI1jbOb/ZM1jbz9YjIbgwhrOqXXbJsbMre1FMjFx7DjlWRsIDlJCma2f4Xs2if9eVgU/+gh3Q6pA5vuzWiwNonhIrRho8N11zJ+yp0zJwxKNC5UkJ2Y8SoHIVQui2CM4Z6X9kuTmFytCs7yLAKo5G2cSoMxZ863RDQceaHfJKN4h/7VOaePzN4hHV9dbKjnRay8FSgyur6VsWuylZLrzBJksTKtnAMzhDT8dKIReFn/kelwzmP0R3c5vtZLk8qjabbKpghzaAslpcLrEjOECD7lF/ygaKXbEkp+PKk5/rnb7n+o5+TLY50igXwMqQ0ncy/BPw1MhMNUmie4+u92qDj/VHlQLhRlf02jrTZv43AKcQGoK65AhZZ0p055BmlFTem1M4XnX8aI15fZR2IkZDlO0vSL/DgEfe/n1OsnS93yPDBJ73tG4nCLnzekLj6Zrt98E5dyA8rzd9F/Z5UC7cBIOjyWkDrrtDYAAU5YESIxLPsD8w43YcDU0qOBLWYOeXcqwym/OUqdsyFdI4QuTL8Iv5t2OPykXw00QsGLaygwoYLdFijAulqZVifYD/3i94bFW4MskwyQbq52xW5TTdPaiPqDOoH7TYhBdf+VNuRdsWWmLWEmRyDMNhOfGkcUAKXDWrkMZiCWrIXYSuIJsZnnnoIWOr5EtJz5VSVrAb/joFfAK/U9ykf782xyMJ0++rV0wsgsyFyDoGG2miXS2hykiUESm1uhfEtkQlG0l6GlJNArbldHN1X6elOV11gZ4XA0uA8FtbzHxnId82NQVCqBNmrU2g8

Hi,

On 22/04/2020 22:36,
jonikelee AT gmail.com
wrote:
> I'm using Coq 8.11.0. Could someone verify that this isn't only me
> doing something stupid?

I can reproduce the bug. (Coq version 8.11.1)

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Jason Gross, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Tej Chajed, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
  - [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] Ltac2 retraction bug?, Maximilian Wuttke, 04/22/2020
      - Re: [Coq-Club] Ltac2 retraction bug?, Pierre Courtieu, 04/23/2020
        
        Re: [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/23/2020