Warns about inconsistency of generated name in evars and goals.

See bug #1041
Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-goal semantics of tactics.
CHANGE: document the features of the new tactic engine.
CHANGE: add Derive.
CHANGES: yellow in Coqide.
A slightly more fine grained way to check whether a TACTIC EXTEND is global or local to goals.

Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
Adds a cycle tactic to reorder goals in a loop.

[cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
Add a tactic [swap i j] to swap the position of goals [i] and [j].

If [i] or [j] is negative goals are counted from the end.
Document cycle tactic.
Document swap tactic.
CHANGES: cycle and swap.