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.
Removing dead code relative to or_metaid.
Qualified ML tactic names. The plugin name is used to discriminate
potentially conflicting tactics names from different plugins.
Code cleaning in Tacenv.
Adding a tclBREAK primitive to the tactic monad.
CPS-style tactic matching. We use the tactic monad as the target of the CPS.
This allows for tail-rec calls, prevents unwanted capture of closures and
results in an overall more efficient evaluation.
Pp compiles after feedback
Pp: only one default feedback id
STM: print goals with no duplicates
make a few lines fit the screen