The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 04/23/2014 01:46 PM, Arnaud Spiwack wrote:
> Well, indefinite description is incompatible with the impredicativity of
> Prop anyway. Definite description is compatible with Coq, but is indeed
> incompatible with erasure.

Interestingly, the IList code appears to work without the 
-impredicative-set flag.  Are you sure it needs it?

> I have indeed implemented a set of proper backtracking primitive in trunk.
> The main one is called "+" (use as t1+t2) and properly backtracks on
> subsequent failure. Now, I don't know what exactly you are after, hence I
> can't give you more precise advice.

I was primarily using eauto, so I will have to create my own 
try-different-things tactics that use +.  I have yet to try that, so I 
don't know what will be needed in addition to +.

-- Jonathan