The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 11/13/2015 01:56 PM, Jason Gross wrote:
> Is [abstract (rewrite in |- *; admit)] faster than than [rewrite in |- *; 
> admit]?
> 
> There's a vernacular (or tactic) that compacts the evar map, right?

Are you thinking of [Optimize Proof]?

> 
> On Fri, Nov 13, 2015 at 1:50 PM, Pierre-Marie Pédrot 
> <pierre-marie.pedrot AT inria.fr
>  
> <mailto:pierre-marie.pedrot AT inria.fr>>
>  wrote:
> 
>     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