Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, May 15, 2014 at 12:10:45PM +0200, Strub, Pierre-Yves wrote:
> Hi,
> 
> This is more a "is this a bug or a feature?" question.
> 
> Shouldn't [rewrite ?foo] succeeds when the rewrite fails due to a dependent
> rewrite error?

The class of failures that are catched by ? is even larger that that.
Just try "rewrite ?banana" or "rewrite ?(I I)" (respectively
non-existing and not-well-typed terms).

It is consistent with the "try" tactical as in "try (rewrite banana)",
so I guess it is not a bug.

Once Georges almost convinced me that it is a feature because if you
chain with ; then the rewrite may be run in two goals with a different
contexts, one of which declares "banana".  So a catch-all ? may help
factoring boring subproofs.

My 2C
-- 
Enrico Tassi