The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> I had trouble understanding the behavior of "move".
> 
> For example, see this proof:
> 
> Goal forall a b c :Set, True.
>    intros.
>    move c after a.
> 
> The hypothesis c is now moved before a. But as I understand it, c should be 
> moved between a and b.
> Why is that?

The word "after" is probably not the best chosen one here. The word
"beyond" would have maybe been better chosen. 

If c comes before a in the order of dependencies (i.e. lower on the
screen), "move c after a" moves c after a in the order of dependencies
(i.e. below on the screen a).

If c comes after a in the order of dependencies (i.e. upper on the
screen), "move c after a" moves c before a in the order of dependencies
(i.e. above a on the screen).

The reason for a "beyond" meaning rather than for a meaning based on
the dependency order is that "move c after a" would be meaningless if
c is already after a, and, at the same time, there would have been no
way to say move c before a if a is the first hypothesis of the
context.

Hugo Herbelin