Documenting option -type-in-type.
Restoring non-uniform delta on local and global constants in 2nd order
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
Printing evar instance in a more intuitive order.
Merging some functions from evarutil.ml/evd.ml.

- Removed collect_evars which does not consider instance
  (use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
  evars_of_filterered_evar_info instead). This is consistent with
  printing goal contexts in the filtered way.
  Anyway, as of today, afaics goals filters are trivial
  because (if I interpret evarutil.ml correctly), evars with
  non-trivial filter necessarily occur in a conv pb. Conversely,
  conv pbs being solved when tactics are called, there should not be
  an evar used as a goal with a non-trivial filter.
do not explode if a plugin is not up to date on -help (Close: 3673)
typo
CoqIDE: new message to print AST
Notation: option to attach extra pretty printing rules to notations

so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).

Available syntax:
- all in one:
  Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
  Format Notation "a /\ b" "latex" "#1 \wedge #2".
XML pretty printing for AST (work by François Poulain, project DoCoq)

It is not 100% complete, but the main part is there.
Simplify evarconv thanks to new delta status of projections,
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
Add syntax for naming new goals in refine: writing ?[id] instead of _
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.

Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
(the action is "clear").

Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.

Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
Add a bunch of reproduction files for bugs.
Add a bunch of reproduction files for closed bugs.
Removing test for bug #2080.

Naming a Ltac definition like a built-in tactic used to fail, but now only
spits out a warning. This is too complicated to test...
coq_makefile: build and install *top.cmxs plugins

These plugins, like coqidetop, stmworkertop and tacworkertop are
intended for toploop replacements (see -toploop command line option).

With this commit coq_makefile can be used as the build system for
any user-interface-specific plugins.
Add additional location information to AST XMLs.
Factored out IDE goal structure.

The more structured goal record type of CoqIDE is also useful for other
interfaces (in particular, for PIDE). To support this, the datatype was
factored out to the Proof module. In addition, the record gains a type
parameter, to allow interfaces to adapt the output to their needs.

To accommodate this type, the Proof module also gains the
map_structured_proof that takes a Proof.proof and a function on the
individual goals (in the context of an evar map) and produces a
structured goal based on the goal transformer.
STM: report the (structured) goals as XML

The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.