The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 13/11/2015 17:43, Jonathan Leivent wrote:
> So, "rewrite in |-*" is carrying around some burden from prior subgoals
> in the same proof.  Perhaps it is performing the search on the entire
> proof term up to that point (which is large if I don't do those admits
> or abstracts), instead of just on the particular subgoal's context?

I don't see where it could be doing so, but that's difficult to judge
without a test-case... The only thing that grows up during the proof is
the evar map, but it shouldn't affect tactics except marginally.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature