Ssreflect Users Discussion List

[t x <>]

Hi,

  Suppose I have something like

H: forall a b, (3 < 5) -> a + 3 = 2 * b
==============================

 .... a + 3 ...

  In non-ssreflect Coq, I can do something like:

  rewrite H1 in H2 by omega, where "omega" is used to solve (3 < 5).

  Ssreflect, however, takes over the meaning of "by."

  Now, is there some way in ssreflect for me to say:

  rewrite H in the goal, try to solve required premises using Tactic, and have the rewrite fail if the premises can't be solved with Tactic.

Thanks!