coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.9+beta1 is out!

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq 8.9+beta1 is out!
Date: Tue, 6 Nov 2018 09:31:43 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f170.google.com
Ironport-phdr: 9a23:ESqGdRJjmQb56++8htmcpTZWNBhigK39O0sv0rFitYgRL/nxwZ3uMQTl6Ol3ixeRBMOHs60C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNxzJXZYJ2WOfdkYq/RYd0XSGhHU81MVyJBGIS8b44XAucfOeZftYz9qEUIrRuiHQaiHuLvyiNRinLo2a01yfkhHhzY0wwkAtkDt2jbrM30NKcOTe+1yLPHzSjeYPxI3Tfw84fIchU7rvGNWbJ8a9beyU4qFw7ciFibtI/rPyuN2+gTr2SW6/BsWOGvhmI9tQ19vCajyt0xhoTLmo4Z0lDJ+TljzIorOdG1SVR3bcC4HJZfrS2XNI17Sd44TW5yoiY10LgGtIa7fCcUzJQnwAbSa/mdfIiJ5hLvTf+RITRliH58drKzmhS//VS6xu3zUcm011lKri5bndXWqn8N0BnT5tCGSvt74EihxS6C2x7P5uxAO0w5lqrWJ4Q/zrIuiJYfq1nPEy3qlEnuia+ZbEQk+uym6+T9ZbXmo4eROJNsigH/LqQhhsi/Dv4lMgcTQWeb/f+x1LLm/ULjQbVKiuc6nbXesJDfPcgbvLK2AxdJ0oY/7BayFyup0NMBnXUeMF1FfA+HgJPyNlHVIPH4CO+/jE62nDdqwfDGJLzhDY/XInjNireyNYp6vkVb0U84yc1Vz5NSELAIZvzpCWHrs9mNJRu4NgGy39HfCck4/YcXRG6CBufNO7vTrVSM7/8jLu2ka4ocuTK7IP8gsa29xUQlkEMQKPH6laAcb2q1S6w/chepJEH0i9JEKl8k+w83TejkklqHCGcBaHO7XqZ67TY+Wtv/UdXzA7u1ibnE5x+VW4VMbzkfWF+JGHbsMY6DXqVUMX/AEopaijUBEIOZZcoh2BWp7lGozrNmKq/N+XRdu8u8jJ564OrckRx0/jtxXZyQ

On 06/11/2018 05.14, Théo Zimmermann wrote:
> Why would you use repeat (intros ?) instead of intros * exactly?

I don't typically write [repeat (intros ?)], but I've definitely written
things like [repeat (intro; try apply xxx)] as part of larger tactics.
Here's a simplified example:

Goal forall A B C, (A -> B) -> (C -> A -> B).
intros A B C H.
repeat (intro; try apply H).

Clément.

[Coq-Club] Coq 8.9+beta1 is out!, Guillaume Melquiond, 11/06/2018
- Re: [Coq-Club] Coq 8.9+beta1 is out!, Beta Ziliani, 11/06/2018
  - Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Beta Ziliani, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Clément Pit-Claudel, 11/06/2018
    - Re: [Coq-Club] Coq 8.9+beta1 is out!, Ralf Jung, 11/16/2018
      - Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/16/2018
- Re: [Coq-Club] Coq 8.9+beta1 is out!, Théo Zimmermann, 11/08/2018