Ssreflect Users Discussion List

[Georges Gonthier <>]

> I'm wondering if we happen to be too strict.  Today we ask, beforehand, the 
> rewrite tactic if it can handle the head symbol of the rewrite rule 
> provided by the > user.  We could maybe say: "if it's not Leibnitz, and 
> it's not unfoldable, then we pass the ball to Coq's rewrite anyway and let 
> it complain".  

   The real reason we unfold is to identify the LHS and RHS, which we need to 
interpret the pattern (at the very least, to skip trivial rewrites). Assuming 
Coq now does the unfolding properly (which was not the case at some point) we 
could otherwise just pass the rule to the Coq rewrite code.

> Another option would be to add a command like
>  Ssr Rewrite Delegate head1 head2 ....
> and keep a database on the plugin side.

That's a bit redundant, because vanilla Coq uses instances of the Relation 
class exactly for this purpose, and nominally the function we call just 
checks for such an instance. I'm not sure why it's failed again (maybe 
because the Coq rewrite bypasses it and directly gets the full instance), but 
it would be better to get the fix from Matthieu instead.


Best,
Georges