Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Jan 13, 2016 at 05:05:22PM +0000, Georges Gonthier wrote:
>  - We use a function provided by the setoid API to determine whether
>  arguments to rewrite are valid relations; it has a history of falling
>  back behind the rest of the setoid library, unfortunately...

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

Robbers, is your rewriteable relation a defined (i.e.  delta-reducible)
constant or it is an inductive/hard constant?

Another option would be to add a command like

  Ssr Rewrite Delegate head1 head2 ....

and keep a database on the plugin side.

Best,
-- 
Enrico Tassi