coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Very slow failing apply

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Very slow failing apply
Date: Sat, 19 Aug 2017 22:34:19 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:k3jMLBebnU/SHcyYflaCYnSIlGMj4u6mDksu8pMizoh2WeGdxc67YB7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpRZbIBj0NBJ0K+LpAcaSyp3vj6Hhs6HUNj9PjjCwe686Dw+7pw/crNJe1Y5rK6IwzBTNo2BUYMxMwmliKEiPnAzx7M295oUl9SAG6Nw78MsVXI3qL/x+SqZXRHQLNmEx5cqjlxTY3xDHyXIYVmgZlVJhGQnM91CpDd/KriLmu78li2GhNsrsQOVxAGz64g==
Organization: X80 Heavy Industries

Robbert Krebbers
<mailinglists AT robbertkrebbers.nl>
writes:

> Suggestions on avoiding this issue are very welcome!

I am not apply lawyer but I have seen people switching from `apply H` to
"refine H || refine (H _) || ... refine (H _ _ _ _ _ _ _ _ _)" [or just
`apply: H` in Coq 8.7/ssreflect] quite a few times.

It could maybe help in your case.

E.

[Coq-Club] Very slow failing apply, Robbert Krebbers, 08/17/2017
- Re: [Coq-Club] Very slow failing apply, Pierre-Marie Pédrot, 08/17/2017
  - Re: [Coq-Club] Very slow failing apply, Robbert Krebbers, 08/17/2017
    - Re: [Coq-Club] Very slow failing apply, Pierre-Marie Pédrot, 08/17/2017
- Re: [Coq-Club] Very slow failing apply, Pierre-Marie Pédrot, 08/17/2017
  - Re: [Coq-Club] Very slow failing apply, Robbert Krebbers, 08/18/2017
    - Re: [Coq-Club] Very slow failing apply, Ralf Jung, 08/24/2017
- Re: [Coq-Club] Very slow failing apply, Emilio Jesús Gallego Arias, 08/19/2017