coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- 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
Archive powered by MHonArc 2.6.18.