Parsing of Type@{max(i,j)}.
Fix bug #3591: print differently eta-expanded projection implicit application and
primitive projection when they would otherwise be ambiguous.
Removing the XML plugin.

Left a README, just in case someone will discover the remnants of it
decades from now.
Removing the documentation of the XML plugin.
Removing dead code relative to the XML plugin.
Removing antiquotations in Tauto.
Fixing TestRefine test-suite file.
IDECDEPSFLAGS is for byte, not opt
Installer for win32

Not 100% functional, but coqide works.

The native compiler is embedded but:
- some path mangling problem prevents it from working even when run via
  cygwin (like in the build process)
- CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run
  (coq should do it).

fix
toploop plugins taken into account when printing --help (close: 3535)

E.g.

Coq options are:
  -I dir                 look for ML files in dir
  -include dir           (idem)
  [...]
  -h, --help             print this list of options

With the flag '-toploop coqidetop' these extra option are also available:
  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE
IDE: disable editable text area underline when -debug

This way a user *can* use coqide with -debug
Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
BackTo not part of the doc when used by emacs

Used to work "by chance".
Back: print subgoals as in 8.4 (Close: 3585)
Documenting the new Undo semantics
A marshalling failure does not make a worker `Old
Marshalling errors should be bold and red (should never happen actually)
Load Prelude.vi if not Prelude.vo is found (Close: 3595)
IDE: escape popup text (close: 3600)