Use an AST for strategy names.
Oopps.. fixed the .ml not the .ml4
Replace the list of argument in tacexpr with a single row argument.

This has several benefits
* It replicates the "no quadrillion-uple" pattern at the level of types. Giving names to the various component will hopefully make for better error messages.
* It is less typo-prone, as the whole row can be passed as an argument rather than retyping each of the arguments. Also makes for a terser [Tacexpr].
* More importantly: local changes to tactic expressions will more often be kept local. Which will avoid some extra tedious work, and make rebases on top of such changes significantly easier.
Discontinued xml plugin: improve the README.

More information, less pmp.
Commit 682aa67cc80 about enforcing that apply does not create new
evars was too liberal. Using an intermediate criterion which makes
both tests apply.v and 3284.v working.
Fix source of initial goal.
No plural for only one non existing focused goal.
Referring to evars by names. Added a parser for evars (but parsing of
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
Parsing evar instances.
Uniformisation of the order of arguments env and sigma.
Use evar name to print goal.
Add syntax [id]: to apply tactic to goal named id.
An old typo which was preventing example #3537 to work the same as it
was working in 8.4.
Fix base_include due to change in argument order of env and evar_map
While we don't have a clean alternative to Clenvtac, add a primitive
for tclEVARS which might solve existing goals.