coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] backtracking issues in extern hints

From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] backtracking issues in extern hints
Date: Wed, 15 Oct 2014 11:33:18 +0200

Nevermind, it is not the case anymore.

It seems that [auto] will backtrack on backtracking hint extern, whereas [eauto] will not. The subtle differences between these two tactics are not a very good thing. To say the least.

[Coq-Club] backtracking issues in extern hints, Jonathan, 10/14/2014
- Re: [Coq-Club] backtracking issues in extern hints, Pierre-Marie Pédrot, 10/14/2014
  - Re: [Coq-Club] backtracking issues in extern hints, Pierre-Marie Pédrot, 10/14/2014
    - Re: [Coq-Club] backtracking issues in extern hints, Jonathan, 10/14/2014
    - Re: [Coq-Club] backtracking issues in extern hints, Arnaud Spiwack, 10/15/2014