Ssreflect Users Discussion List

[Ralf Jung <>]

Hi,

>>> 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.

Seeing these examples, you're probably right. The default behaviour of
eapply works well for many, but not all cases.
The reason why I suggested making it the default is that I stumble upon
cases like the one you mentioned above rarely (if at all), but I often
use existentials the way eapply does - so I wouldn't want to write
"apply: H; hide_existentials" all the time. But well, I can just use
eapply instead.

Kind regards
Ralf