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.
make a few lines fit the screen
Goal: API to get the solution of a goal
new "all || :" goal selector, like "all:" but in parallel

E.g. "all |4| : tac" runs tac on all goals using 4 workers
STM: code restructured to reuse task queue for tactics
STM: Implementation of "all |n| :"
New test for "all |n| :"
fixup stm refactoring
Coqide: annoying popups with GTK errors only in debug mode