Fix misleading pretty-printing of information for non-universe-polymorphic
definitions.
A handful of useful primitives in Proofview.Refine.
Distinguish tactics t1;t2 and t1;[t2..].

They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently.
Start documenting universe polymorphism.
Forgot to add a Universes.v.tex as a target.
Fix handling of universes at the end of proofs, esp. for async proof processing.
Thanks to E. Tassi for the initial patch.
Fail gracefully when focusing on non-existing goals with user commands.

Fixes bug #3457
Small reorganisation in proof.ml.
Add lia.cache to the .gitignore
Add *.crashcoqide files to the .gitignore.

They occasionally show up while testing. I think it cleaner to ignore them.
Add emacs auto-save and crash-save files to the .gitignore.
More documentation of universes.
- Do module substitution inside mind_record.
- Distinguish between primitive and non-primitive records in the kernel
declaration, so as to try eta-conversion on primitive records only.
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].