Fixing bug #2900 (evar/evar unif was supposed to be treated in
solve_simple_eqn but in case the second evar was hidden behind a
local variable, it arrived in evar_define and imitate, wrongly
assuming progress).
Propagating conversion_problem towards (postponed) evar/evar problems.
Incidentally simplifies where evar/evar problems are treated (in
evar_define and imitate rather than solve_simple_eqn).
Updated debugging printers
Evars introduced by Proofview refining are flagged as GoalEvar. For some
reasons, some code depends on it.
Better error message when found more than once object of name ...
Fix Bug 3217

Normalize the term to see if there are arguments to daclare implicits only if
at least one argument occurs in the non normal form
Fix Bug 3131 + Really drop mentions of info in refman.
STM: be more resilient to explicit Back + Sideff commands (closes: 3251)
Add a test case for bug 3251

It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca.
A debug printer for Evd.Filter.t
Clean up the .merlin

I added a .merlin in ide/ who inherits everything from the root .merlin and also
adds the dependency to lablgtk, which I removed from the root file. These way
people not working on that part of the code won't get bothered if they don't
have that package.

I removed the S/B entry for plugins which was useless, indeed there is no ML
file in that directory and merlin doesn't scan the subdirectories recursively
(as you know).

I also removed the S/B entry for checker since most of the files of this
directory are also present in kernel and that was the cause of a lot errors on
merlin's side (think "inconsistent assumptions").
On top of that, no part of the tree depends on checker (I back that assertion by
a grep of the *.d files of the tree) so these lines in the .merlin were actually
useless. The only part of the tree where you need to know what's in checker/ is
when you are working in checker/ itself, but since merlin automatically adds the
directory of the file under edition in its source and load paths nothing else is
needed.

There might still be problems after this patch, but they should be less of them.
Considering my poor knowledge of the codebase there might be other conflicts I
have missed.
Remove option -g as it is non-portable yet does not have any effect on the test-suite. (Fix for bug #3024)
Support other forms of "Proof" in coqwc. (Fix for bug #2735)
Fixing #3262 which revealed a non-progressing, hence looping,
refinement of evars (in filter_candidates).

Incidentally introduced a copy of type "option", "update", which
highlights the specific intention of "updating" or not.
Fixing coqchk. It was my fault, I misused canonical and user equalities
when defining cache hash tables in Closure. Why it was working in 3.12
is a mystery to me.
Prevent verbatim text from leaking out of comments. (See bug #2882)
Closing bug #3164
Recognize "Instance" in coqwc. (Fix for bug #2551)
fixing Function doc
Fix for bug #3107.