coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] structural specification of where to unfold

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] structural specification of where to unfold
Date: Sat, 29 Sep 2018 18:28:32 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:kzE6lxWURPpYVLr3ju8mpmwpuULV8LGtZVwlr6E/grcLSJyIuqrYYxSBt8tkgFKBZ4jH8fUM07OQ7/i/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9wIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kr9VrhGvpxNw34HbfY6bO/hwca7GYdMXRnZNUtpNWyFbAI6xaZYEAeobPeZfqonwv1QArR2kBQmtGOzvzSJDiGHs0q0hyOQhEBzN0Qs+ENIIqnTUrcn6NKAIXeCp1qbI1i7Db/JN1Df87ojIaBEhruuWUbJ+a8rc0E8iHB7LgFWXrIzqJTKV1uIVvmia6epgT+OvhHQ9pwF/uDiiwNonhIrRho8Nzl3J+j91zJg7KNGiSUN2ZcSoHIZOuyyYMYZ9X9ksTHtyuCkgz70LoZ67czYOyJQg3xPfZeKIc5SU4hL+UuaRPS13iGhieLKliBa+6UmgyuviWcmoyFtHqiVInsPSun0DzRDe68yKRuFg8ku/2zuDzwXT5ftFIUAwm6rbMZkhwrsom5ocq0vDBDH5mF7tga+YaEok5vSo6/nhYrX6vJCQLYh0ihvxMqg2gMywHfw4MhQSX2ic4emzyLrj/VTgTLpWiv02j7LWvYvBJcUbo665GxVa3pwi6xa5FTem0c4XkWMJLFJfK1q7iN3iPEiLK/TlB9++hU6tmXFl3aPoJLrkV7jLNHnIl//ddK1m6gYIxQwpzNtYoY5dEaoACPP1QE748tLCWExqezeoyvrqXY0unrgVXniCV/fAYfHi9GSQ7+dqGNGiIYocuTLzMf8gvqK8g3IlhUIbYaDv2oEYOijhQqZWZn6BaH+pue8vVH8Qt1NmHu3sklyLFzBJNS7rAvAMowojAYfjNr/tA4CghLvYgHW1E4FKe2ZaAxaLC3i6L4g=

On Fri, Sep 28, 2018 at 09:58:35PM -0400, Matthieu Sozeau wrote:
> Hi Abishek, ssreflect’s rewrite supports contextual patterns and unfolding
> with “/“. Maybe with `pattern` and `eval unfold in` and `change` you could
> program this in Ltac as well.
>
For reference: https://hal.inria.fr/hal-00652286v2

Best
--
Enrico Tassi

[Coq-Club] structural specification of where to unfold, Abhishek Anand, 09/28/2018
- Re: [Coq-Club] structural specification of where to unfold, Matthieu Sozeau, 09/29/2018
  - Re: [Coq-Club] structural specification of where to unfold, Enrico Tassi, 09/29/2018