Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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.




Archive powered by MHonArc 2.6.18.

Top of Page