The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you are dealing with coinductives, then it's probably the known long-standing issue that Coq's implementation of coinduction breaks subject reduction.  If you have issued [Opaque] commands which would cause the body of the constant you're unfolding to be ill-typed if you were to give it to Coq in the current environment, then it's intended behavior, and unclear which bit should be called a bug.  If neither of these is the case, then it's a bug in Coq, and should be reported.

On Thu, Oct 6, 2016 at 3:03 PM <Marc.Bezem AT uib.no> wrote:

Has anybody observed that an unfold can make a goal ill-typed?
I'm asking this to find out whether this is a coq bug or a user error.

The situation in which it happens is quite complicated, and the
ill-typed goal lived on for quite a while. From the point where the
goal became visibly ill-typed I could trace back (all the time testing
the goal with Check), and the command that first made the goal
ill-typed was a rather harmless unfold. It will be a challenge to
isolate the behaviour in a simple example.

All help will be appreciated.

Marc