coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Very slow failing apply

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
Subject: Re: [Coq-Club] Very slow failing apply
Date: Thu, 17 Aug 2017 20:36:05 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:gePl4Ry7mOw0X+LXCy+O+j09IxM/srCxBDY+r6Qd0e4TIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2TxTor3az9T8fHAnkfUowf7ytW92as8Pi3OervpbXfg9ghTynYLo0Ig/y5T3Qu9MMjM5HI7wwxyzxI3dSfPgekXtpKEiJklP5792x8dh7/ihKvO4J9shaUKy8cb5uHpJCCzFzCWc/7sDxqVHgVwaF7HYGSS1ClxNJBwnD4xX7RYvqmjH9vOBwwjWZJ8D8R70uQnKk6/E4G1fTlC4bOmthoynsgctqgfce+Ur5qg==

On 08/17/2017 06:18 PM, Pierre-Marie Pédrot wrote:

On 17/08/2017 15:45, Robbert Krebbers wrote:

Suggestions on avoiding this issue are very welcome!

What about using the 'simple apply' tactic instead? Is it too weak for
your use cases?

Thanks, simple apply does not suffer from this issue, and at least allows me to compile my development in finite time :).

Do you have any idea what apply is doing what simple apply is not?

[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