Subject: Ssreflect Users Discussion List
List archive
- From: Florent Hivert <>
- To: "" <>
- Subject: [ssreflect] addn0 in Hint
- Date: Thu, 1 Aug 2019 10:54:48 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:rsW1SRbaWVxPAqCcHeNtuq3/LSx+4OfEezUN459isYplN5qZoMi7bnLW6fgltlLVR4KTs6sC17OM9fG/EjRfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmsqQjctMYajZdgJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKxVrhK/qRJiwIDbb52aO+dwca7GYdMWWXZNUtpNWyFbHI+xaZYEAeobPeZfqonwv1sArR+5BQm2GuzvzCNIjWL00607zeQuDxvG3BA9FN8JsHrUqNL1NL0MXuCz0KnE1zfNb/JI2Tjj8ojIbgssofWWXbJxa8bRx1MvGhrDg16NqoLlJyuY2vkTv2Wf9eZsSOCihm49pw1sojWj3NoghpXPi4kI0F7L7z95z5wwJdCgSE50f9qkEJxIuiGfLYR2Q8ciTH9nuSYm0LEGvYS7fCkQxJQp3R7Tc/2Hc46W7RL/TOudPCl0iXZ/dL6ihRu/8VKsxvD8W8WuzVpGsjJJktzWuXAM0xzT5NKHSvx4/kq52TiP0wfT6vtaLkAyiarXMZwvwr8ulpUNq0TDAjT7mEHsjK+XbEkk9PKo5/z9Yrr6vp+cK5N0igbmP6Q1gcy/G/o3MgYKX2eF5eu8yKbu/Vb5QbVPlv05iLPVsJHcJcQBp662GRVZ0og560X3MzDzms8Dh3QJKF9OZDqClJKsOlfUIfm+DPGlgl3qni0hj6TdJafsDJHAJWTrlaz7OLd78U9Vjgs119FWoZxOXOIvOvX2D2H1s8bVCANxEw2qzvz7QIFT0oQEVGSTRI+YLq7IrXeM/ONpLfPaN9xdgyr0N/Vwv62mtnQ+g1JIJfD1j6tSU2ixG7FdG2vceWDl0oUFC2ZMsBBsFLW72m3HaiZaYjOJZ4x54zg6DIy8CoKTFIS3gfqPxnXiR8AEViV9ElmJVEzQWcCEVvMLMXzAJ8ZgljEUSf6lUY5n2wv87AI=
Dear all,
The following used to work:
Lemma bla (n : nat) : n + 0 = n.
Proof. by []. Qed.
It doesn't work anymore with MathComp 1.9. Is it on purpose ?
Best,
Florent
- [ssreflect] addn0 in Hint, Florent Hivert, 08/01/2019
- Message not available
- Re: [ssreflect] addn0 in Hint, Florent Hivert, 08/01/2019
- Message not available
Archive powered by MHonArc 2.6.18.