coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
- To: Coqdev <coqdev AT inria.fr>, coq-club AT inria.fr, coq+announcements AT discoursemail.com
- Subject: [Coq-Club] Coq 8.19.1
- Date: Mon, 4 Mar 2024 13:58:15 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.helo=postmaster AT relay9-d.mail.gandi.net
- Ironport-data: A9a23:6nU4HqAJpNhhChVW/4rnw5YqxClBgxIJ4kV8jS/XYbTApGtxhDVWy GdNWTuDb/jbY2fyfIoiaIvn9hhXsMfUytFgOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHZjdJ5xYuajhIs/nb9Es11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc5xb8fSG3x/ZBN01oBc4m5OpXPW1qq cVNfVjhbjjb7w636Ki2TuB914EvasziPYdZtXhmwTCfC/s6KXzBa/+TupkHhHFp1psIRKePD yYaQWIHgBDobBRCJl4RTp0/mO2lnGXXaD5Js1GUoK86+S7VwRAZPL3FYIOPIIDVFZQ9ckCwq mjf9nTTDCgmHv+a8wu4rXeMie/MgnauMG4VPOfprqE23QX7KnYoIBYRTB6wpeSzolWvXspWb U0S4Csn66YonGSgScDxUgOQu2+BphdaWtxKEuR85hvl90bPyxyUAmEVH3tNLtkvtctwSjUs2 l7Pmd71bdByjFGLYSmn+O3PqTCdAiRLFSw8eyMkcQchv+C29enfkSnzZtpkFae0iPj8Fjfx3 y2GoUACa1M70JNjO0KToACvvt68mqUlWDLZ8S35ZAqYAu5RfoOhbp35rFSd6P9BKMCWR1+Nv T4CltT2AAEy4XOlxHblrAYlRunBCxO53Nv03QcH834Jq2nFxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOt3pWph7lfaxSY66CJg4i+aihLAsK2drGwkwPSatM5zFzBBEfVwXZ c/KL57E4YgyVfs5pNZJewvt+eV6nn9imDu7qWHTwB2h3bvWf3eOIYrpw3PQBt3VGJis+V2Pm /4Gb5Xi40wGAIXWPHOLmaZNdgtiBSZgWvjLRzl/LbLrzvxOQzx5V5c8ANoJJ+RYokiivr6Yp CDnBxEGlQOXaL+uAVziV02PoYjHBf5XxU/X9wR2Vbpx8ylyPdSc/+0EeoEpfLIq0uVmwLQmB 7MGYsiMSLAHADjO5z1XP9G3oZ1AZSabo1uEHxOkRzwjIL9mZQjCoeH/ciXVqSIhMyuQtOkFm YOG6D/1e5Q5elldPJ7kU873l1KVlloBqd12RHrNc4Vyel2z0Y1EKB7Rr/4QIuMeIE7H1DLA0 xqcPikJgeyQp4Me0cLogJqcpNyDCNpOHUt9Hkja442pNCLcwHGR/I9YXMuMfhHfTGnR+pj+V d5Kzvr5DuILrGxKv6V4Dbxv66A0vPnrmJN30SVmGy/tQ2mwK7Y9PESD49ZDhpdNypBdpwGyf ECFofteGLeRPfLaAEwjHxUkYsuDxMMrtGHrt9ptG3rD5Qhz4LajemdRNUPViCVicZ1EALl8y uIl4MMr+wizjyQxCem/jwdWyn+tK0IRWKB2p7AYB47W0jAQ8G9gWqCFKCHK48CoUe5uY20KO T6fgZTQi4tMnnTid2UBLlmT/O5/q6lXhjV04g4jHWmZovvEmf494zNJ+xsVUAl+70tKwsBzC EdRJmx3IqSF+glztfhAAkSTIhxLOzOB8GeszWo2yW7QdBS1ZFz0LUkWG+WEzGYG+U1yIxlZ+ 7C5zj7+cDDIJcve4Ao7aXRHmdfCE+Nj0xLkmd+1Oui4BLw4XGbVubCvbm82tBfXO8M9q0nZr +1M/uwrS6nEGQMPgq88Ua+26K8xTU2aGWl8Xv1RxqMFMmXCcjWU2zLVCUSQeNtIFsPa432DF M1iCcJeZSuQjB/UgGggOpcNBLtokNoCxtkIIOrrLFFblYqvlGNitZaI+xXugGMufc5Vrv88D YHsbBOHLH2bgCpFum3KrfQcAFGCX/s/WFTe0ty2ocIzLLBSlMF3cEo37Km4gGXNDitj4CCvn V3iY4348rVc7LpCzqrWPIdNPQGWEe/Idf+p9VmzuutebNmUPsbpsRgUm2bdPA9XHOUwXfJtm ISrqtfIhV/3jJcrWWXnw7iACKh7ysGgV8VHMs/MDSd7nAnTfOTO8hc862SDBpgRq+xk5+6jX BqeVMu8UfU3SuVt7iRZRAYGGilMFpmtSLnroB2MisilCz8f4FThF8ym/3q4VlNrXHYEFLOmA zClpsv0wM5TqblNIxo2B/tGJZtcC327UIsEc+zBjxWpPlOKsHij5IS7zQEB7AvVAEaqCMz5u JLJZibvfSSI5Z3n8otrjJxQjDY2UlBGnugCTmAM8YVXihe7LlI8A8YzDJEkMqxQwwvOjMzWR TeUYGUbXHC3GXwOdBjn+93sUzuOHuFEaJ+zOjUt+FjScCusQp+JBLx67Cp7/nNqYX3Zwfq6L c0FsGjFVvRrLkqFmc5IjhB6vQtm+h8e7mgF/Unswon+RRMXALFM23VnEAsLUyHbey0IvFueP nA7HAioX2niIXMd0+45E5KWJP3dlCjs3i4rbCKKzcyZvYiHpAGF4OOqIPn9i9Xvc+xTTIPjh hrLq6+l+GOHwX8SvK4koZQvjLMc5Tdn2CSlBPeLeDD+VJ1cJojq0w3uUMbPoAwfFNZjLm7g
- Ironport-hdrordr: A9a23:Fi4I7ajEb1JowCqyHAdc37vf33BQX0513DAbv31ZSRFFG/FwyP rCoB1L73XJYWgqM03IwerwXpVoMkmsjKKdgLNhdItKOTOLhILGFvAH0WKP+Vzd8k7Fh6ZgPM VbAs9D4bTLZDAU4/oSizPIcOrIteP3lZxA8t2urUuFIzsLV4hQqyNCTiqLGEx/QwdLQbAjEo CH28ZBrz28PVwKc8WSHBA+LqL+juyOsKijTQ8NBhYh5gXLpyiv8qTGHx+R2Qpbey9TwI0l7X POn2XCl+ieWrCAu1PhPl3ontprcejau5p+7Qu3+4gowwDX+0mVjUJaKv6/VX4O0aOSAR0R4a HxSl8bTr9OAjXqDyqISFLWqnTdODpC0Q6Z9XaIxXTkusD3XzQ8Fo5Igp9YaALQ7w46sMh7y7 8j5RPsi3P5N2KwoM3R3am7a/hRrDvAnVMy1eoIy3BPW4oXb7Fc6YQZ4UNOCZ8FWCb38pouHu ViBNzVoK8+SyLtU1nJ+m10hNC8VHU6GRmLBkAEp8yOyjBT2HR01VERysATlmoJsJg9V55H7e LZNbkArsA4cuYGKaZmQOsRS8q+DWLABRrKLWKJOFziULoKPnrcwqSHk4ndJNvaCKDg4KFC5q gpCmkoyVLaU3iedvGz4A==
- Ironport-phdr: A9a23:FG051xCKKCHH1seccvG0UyQUmEoY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua88ygKWFtmAo7Ic0qyK6fCmATRBqb+681k8M7V0FCU5wf0MmAIhBMPXQWbaF9XNKxIAI cJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+N hq7oRvVu8UMgYZvKKk9xxTHr3BVf+ha2X5kKUickhri5cq85oJv/zhVt/k868NOTKL2crg3Q rBfEDkoKWc56tH1uxLeVwWP/HwcUmsXkhpMHQfI6QzxU4nyvCXnqOdzwTGWMsLqQ786XzSi9 LprRwTziCgbLT458XrYhdJ2galGvR+uvR1/w4rTYIGIKPpze77WcN0GSWZdWMtaSipMCZ6+Y YQSFeoMJeVWoYfyqFQAsxWwBRSiC//gxDJTmn/73rc33/g9HQ3Y3gEtGc8FvnTOrNXyMacfS eG7w7PUyjXfdfxW3yr25onJchAluv6DQ6hwcdbMwkQoGAPKlEufqZD/MDOTzOgNvGmb7+57W u2xkW4ntxp8oiOsxsYskYnJhYMVylXB9Spn2oY5P9u4R1BnYdO9FpZbqi6VOZdsTMw4X2Fop Dg1yqcAuZOjYCQG1pQpyh/DZvKIbYSF4gzuWPiPLDp5mX5rd66zihKz/EW91uDwS8m53VJUo idYkNTAq24B2wHR58aHSvVx4kGs0iuB2QDU7+FLO0E0lazDJp4uw74wipoTsVnYESPshEr2i 6qWel0l+uiu8eTnY6/pqoWSN49ujAz1L6cgmtSnDOgmLwQDXXKX9Oag2LH54EH0Q7tHgucrn qTdtJ3XI9kQq7C9Aw9IyYYj9wiwDy273tQZnHgIMkpIdA6BgoP0IV/BOur4Au26g1m0kDdk2 fTGPrr5D5XXMHfDlK3ufLZ55kJF1QU/19Vf6IhVCrEFOv7zVVX+tNrFAR84KQC0xfjoCMll2 oMfX2KAHLOZPbvMvVOV5O8jOeuBaJMPtDrgKPUo6eTigWI9lFIZZaWp2IEYaHG8HvRoOUWZZ n/sj88OEWgQoAU+UPbliFuYXT5cZnayW7kz6S8hCIK6ForDXYOtgbya3Ce4H51WY2VGBU6WE XvycYWLResMZDqUIsB6ijMET6SuS5c91RGysw/306RrIvLO+iIErZLjyMR15+rLmB4u8jx0F t2R3H2JT2FphWwFXCQ23aB6oUxl0FiPy6l4g/pCFdxS/fxFSAk6NYTEw+xgF9/yQh7BfsuOS Fu+XtqmBigxQc8vzN8QeEt9ANWjjhXb3yWwGbMVlrqLBIY18q3GxXTxKdx9mD760/wKiEAqT 9UHYWahn6Jy6SDSAZTImgOXjfDuPa8bxWvG8HqJ5WuIpkBRFgBqFe3OWmlcb03Qqsn/7U7HQ rmyEpwrMxBKztOYMaZPY9zty15BQaTNItPbNk24GHu5A16nx7eGYZD2MzES1SjBAU5CnAEX9 3ucKSAlBTa6oGPbCTF0U1TifxW/oqFFtHqnQxpsnEmxZEp72u/tkvZ0rfmVSvdIm6kBpD9ks DJsWlC0w9PRDdOE4QtnZqRVJ90nsx9czWyMkQt7M9S7Krx6wEYEelF4tk7y3hMxBYREm8Uws FsxzxtpKqOd1V5bMTWVwcO4IaXZf1H75wvncKvKwhfb2deS9L0I7aE3olj/tQfvGUsm+Xh9z /FO0GqH5ZTPCQcIF5T8ThV/7AB08onTeTJ1/IbIzTtsPK2z5yfFwM4sDfA5xwyIZdpbObLVU QO0FsQbA46hIeommh6vYw5s0Pl60qkyMovmcvKH3PXuJ+N8hHe9inwB5olh00WK/i46S+jS3 p9DzevKlg2AHyzxilusqKWV0chNeC0SE2yjyCPlGJ8ZZ6t8epwOAHuvJMv/z8t3hprkUXpVv FC5AFZO1MiscBuUJ1vzuG8YnUserGCun223zjh+nis1hrGczTfNwuHneQBBPGNXBSFjgVrqP YmonoUCRkH7Cmph3BCh5Ev82+1avPEldjaVHh8OJnitaTgzA/jV1PLKecNE5ZI2vD8CVe29Z QvfUbvhu14B1DulGWJCxTc9fjXsu5PjnhU8hnjOSRQ75HffZ8x0wg/SodLGQvsElDUPSTVxj 3/YB1y2MsO11c6XhozAs+W7WnjnUJBPO3qOr8vIpG6g6GtmDAfq1f+6l8HuF0410Cvx2sN2f T7LvQ3/Y4zu2r78N+97NBoNZhe0+49xHYdwlZE1jZcb1C0Bh5mbynEAlH/6LdRR3a+WgGMlf TcQ2JaV5QHk3BYmNXeV38fiUW3bxMJ9Zt68a2dQ2yQn7skMBr3GpLBDmCJ0pBK/o2ezKbByl zoBwP1o538eiewTpCI2zTSGAbEXGERCeyrhi1yE4su/o6NeeGu0OeLpiwwhxZb4XOrE+1ANE H/iH/VqVTd99MB+LE7B3DXo54fodcORJdMfuxuIkgvR2u1cKZY/jP0P1k8FcSr2uXwozfJ+j AQ7h8jl+tffbTw9p+TgU08LU1+9L9ke8Tzsk6tEy8Of3oT0W45kBi1OR5zwC/ShDDMVs/3jc QeICjw17HmBSt+9VUeS7llrq3XXHtWlLXaScTMWxNh+TR/bK01big0OQB0hnY8iFQGvwcH7N kF0+npCgzyw4gsJ0e9uOxTlBy3QrQq0YzFyR5mbJhdM8ilZ5FbOMs2b6+9pWSdV4tfyyW7FY nzebANOA2YTX0WCDF22Jbii6+7L9O2AD/a/Jf/DMv2e7PZTXPCSydezw5NrqnySY96XMCAoX JhZkgJTGGp0EMPDl3ATRjwLwmjTOtWDqk70+zUr/Jrmr7K0AES2utvJUuoIdo8xnnL+yaaba bzK3H4ge2pSh8NeyXSUmuhNjhlM12lvb2X/S+1f83GVCvuAwekOXkRcMXMWVoMA7rpgjFMUZ oiE0pWshuQ+0aRyUA0NVES9yJvwOopVeyfkZAmBWxrMb+7OcjTPx4ufjbqUcbRLl60UshSxv W3eCEr/JnGYkCGvURmzMOZKhSXdPRpEuYj7fAw/QWTkSdvnbFW8ProVxXUuxqYog3rRKWMGG SJxd0pc//icqyZRg/E5FGVH4nsjK+SY0yqU9OjXLJ8KvOAjWH0r0b0Cpi1qkP0MvXAhJrQ9k TCattN0plC6juSDgiFqVhZDsHcDhY6Gu1ljJbSM9pREXiWM9xYM4GOMThUS8oE8VZuw4+YJm oOJzfOie1Igu5rO8MARBtbZMpeCOXslal/yHSLMSRACVXitPH3egEpUlLeT8GeUp940sMuJ+ tJGR7lFWVgyDv5fBF5iGYlIL556Qjoi17GaiMQF/2aWtxrAX8Zbu5XKTLSUDOmle1P7xfFUI gAFx7/1N9FZLorgx0lrcUV3hqzQFk7ZTIEIrmtkZw4w5kpE9nR/CGs+xwi2D2HlqG9WHvmyk BksjwJ4aul47zbg7WA8IV/SrTcxmk08yp31xCqceznrIOKsTJlbXmDq4lMpPMqxEGMXJUWi2 FZpPzDeS/dNgqt8ICp13RTEt8IHELYZRKlAKnf4JNmNavEhwAUZpmOizE5Do+TMD5dj0g0nb cz1x5ql8xlgfcU2JKnVKbAPyFVM1PrmVsCAzeMg2wwfIkMA6iWUdTJa4SQ1
- Ironport-sdr: 65e5c579_UTcPhgQgnkVs1yxL+tBXNMA1pNWZIcYW+NjeePtGr2lMFzn t89susIxhQnPwmEFTj0pIsIOA1iokONUC3BuarA==
The tag for 8.19.1 has been set to commit
8152d125abb0fb7e8cbecf4bd6cd51d8d3e70d78.
Coq 8.19.1 fixes a number of bugs, most notably:
- incorrect abstraction of sort variables for opaque constants leading to an
inconsistency (https://github.com/coq/coq/issues/18594)
- memory corruption with vm_compute (rare but more likely with OCaml 5.1)
(https://github.com/coq/coq/pull/18599)
See changelog for details:
https://coq.inria.fr/doc/master/refman/changes.html#changes-in-8-19-1
--
Gaëtan Gilbert
- [Coq-Club] Coq 8.19.1, Gaëtan Gilbert, 03/04/2024
Archive powered by MHonArc 2.6.19+.