Assume ... yields unexpected behaviour

[pimotte]

In exercise 6 of the tutorial, writing Assume a > 0. instead of Assume that a > 0. does not yield an error, but instead appears to do nothing ( the goal does not update).

This might be a consequence of some default rocq stuff?

[jim-portegies]

@pimotte I cannot reproduce, can you perhaps give more detail?