Ssreflect Users Discussion List

[<>]

Dear Benjamin,

I was not aware of your suggestion, which seems sufficient for my problem;
thank you!

> Problems :
> 
> 1) you have to write the body of the definition once in your command.

This would not be problematic for me; I can use ssr's pose tactics.

> There are indeed two possibly desirable extensions:
> 
> - having a tactical combinator in order to appply a given command for
> every hypothesis.
> 
> - a ssr entry "in *" to do the same of one rewrite item.

I agree.

Best regards,
Keiko