The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Aug 01, 2014 at 11:02:48AM -0400, Jonathan wrote:
> >Ssr POV is that evars are constants, no ssr tactic should let you
> >instantiate them, but should not "destroy" them either.  We hardly use
> >evars in our goals.
> 
> Perhaps the occurrence of evars is much more likely when using backward
> chaining.

Sorry for being naive, but I seldom have evar around even if I
backchain.  Can you give me an example of typical situation in which
you generate a new evar by backchaining?

Best
-- 
Enrico Tassi