Ssreflect Users Discussion List

[Enrico Tassi <>]

I don't know how you debug lines begining with "by" that broke in an
easy way.  The only way I know is by removing the "by", then adding "."
somewhere in the middle.  Once things work again, go back and add "by".

Just adding the "." does not work, beccause "by" still aplies to initial
fragment of the line, and is very likely to fail.

  by toto; titi. (* err *)
  by toto. (* a different err: a subgoal is not closed by "by" *)

I think we could add a "yb" tactic so that

  by toto; yb.

behaves like 

  toto.

So the new way of debugging is by inserting ";yb." somewhere in the
middle of the line, no need to remove "by" nor to put it back.

Does it look reasonable or I should get more sleep?
-- 
Enrico Tassi