Ssreflect Users Discussion List

[Enrico Tassi <>]

As per section 9.9, the semantics of move/v1;move/v2 and move=>/v1/v2 is
slightly different.  In short the automatic generalization of unresolved
implicit arguments is done only at the end of the chain of views.
To break the chain in two single view application one can just write
move=> /v1 - /v2.

When one refactors a script he may be tempted to glue two lines and if
the two lines end/begin with a view application he may inadvertently chain
the views together and incur into a "mysterious" error.

Now, I have completely forgotten why I coded it this way.  I mean, one
could generalize after every view.  I recall there was a reason, but my
memory fails me.

Anyone recalls why?
-- 
Enrico Tassi