Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Apr 24, 2014 at 07:11:36PM +0200, Ralf Jung wrote:
> >   apply: ...; something.
> > 
> > where "something" hides a class of subgoals.  This something is called
> > "shelve_unifiables" in coq trunk (at the OCaml level, dunno if it is
> > exported as a tactic).
> 
> Something like that would be great, yes . and maybe some way to do this
> per default, as personally I don't see a reason to ever not "shelve"
> these evars which appear in other goals - but it seems you disagree on that.

There are cases in which what you ask for is odd.  Eg if you have a
record with a type, some functions on that type and some properties
about these functions and one applies just the constructor of the record
one would get (in the case of a monoid) too few goals like IMO:

  forall x y z : ?T, ?op x (?op y z) = ?op (?op ...) ...
  forall x : ?T, ?op ?e x = x.

Another exaple is when the dependency is shaky, e.g.

  fst x ?e

In this case you may get this as a goal, then simpl, and you loose the
possibility of instantiating ?e.  Hence a mechanism to grab forgotten
evars.  And what happens if this happens in the middle of a huge Ltac
code?  Where do these lost evars come from?

IMO the 1 goal = 1 evar deal is much more sane.
  
Ciao
-- 
Enrico Tassi