The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

In the old implementation of Coq, the type of proofs in progress cannot handle dependencies between subgoals. The issue you have here, I think, is that you need a goal to complete ba', and you expect the result of this goal to appear in subsequent goals.

The new implementation (from v8.4 on) can handle that, but the tactics still "believe" they work in the old v8.3 world. It should all be solved for the next release of Coq though. But it is not without issue (in some cases, refine asks for more subgoals than the v8.4 refine, hence introducing some incompatibilities).

On 1 August 2013 15:09, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

  Thank you!  It works, also I've applied this trick to buf', it
worked too, so I've constructed this function successfully.

  However I can't understand why it works.  There should be some
low-level reasons, and it's interesting to know about them.