The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/01/2015 03:43 PM, Joey Dodds wrote:
> Hi,
> I'm trying to do a mutually inductive proof where Coq puts the lemmas you
> are trying to prove above the line and you have to be careful where to
> apply them or you will fail to QED.
>
> My automation keeps using them, and I was wondering if there was a way to
> define a tactic to temporarily make them unusable. My first attempt was
> rewriting them into an opaque identity function, but it seems like auto and
> apply are happy to ignore opacity and unfold the definition anyways.
>
> Thanks,
>
> Joey

I have a way to do this in 8.5, but it's a bit of a hack (again).  I 
also requested this feature as enhancement #3845.

I'll extract the hiding tactic from some other stuff I'm working on, and 
post it momentarily...

-- Jonathan