Ssreflect Users Discussion List

[Ralf Jung <>]

Hi,

>> One last thing: the leading "by" applies to the whole line, and "by
>> apply" is very much like "exists".
> 
> I guess Enrico meant "exact" here. However, while "by apply: H" and
> "exact: H" are the same, I don't think that "by apply H" and "exact H" are.

*oops* I should have read this mail before replying to the other and
asking this very question there, sorry for that.
I just tried it, and even if "apply: A B" leaves some goals to close, if
"by apply: A B" closes them all, then "exact: A B" also works. That
surprised me (I thought exact: was more like the Coq exact), but well,
it's certainly nice to have.

Kind regards
Ralf