The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/01/2014 11:38 AM, Enrico Tassi wrote:
> 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

An extremely simplistic case of perhaps the most common culprit: 
econstructor (and equivalent uses of eapply, refine, etc. that omit 
arguments in favor of subgoals - i.e. backward chain):

Variable P : nat -> Prop.

Inductive mytype : Type :=
| Mytype(x : nat)(px : P x) : mytype.

Goal mytype.
econstructor.

produces the goal like:

1 subgoals
, subgoal 1 (ID 4)

  ============================
   P ?3

Consider similar construction of instances of types with much more 
complex parameterization/indexation.  The evars occur in the subgoals 
corresponding to omitted (in the constructor application) dependently 
constrained fields in the constructor.  In the above, if we eliminate 
the px field, the subgoal generated is just "nat" - no evars.

-- Jonathan