Removing a Goal.sensitive in Rewrite.
Removing unused parts of the Goal.sensitive monad.

Some legacy code remains to keep the newish refine tactic working, but
ultimately it should be removed. I did not manage to do it properly though,
i.e. without breaking the test-suite furthermore.
Move UnsatisfiableConstraints to a pretype error.
Tactics.unify in the new monad.
Fixing bug #3533.

Now error printing tries to set universe printing when two terms are not
desambiguated.
Fixing ml-dot & mli-dot targets.
Fix test-suite file.
Tactics.is_quantified_hypothesis does not reduce anymore to decide whether
a variable is quantified in the goal. This is only used by induction, and
it should be a bad practice to depend on an invisible binder.
Enabling drag & drop on the source view widgets.

Sort of fixes bug #2765, but the file loading is broken and puts coqtop in
an inconsistent state, so that even the previous half-working patch was
actually not functionning at all. This should be fixed eventually.
Fixing bug #3404.
Removing a unused legacy parsing rule.
Fixing a bug introduced in the extension of 'apply in' + simplifying code.
Fixing previous commit.
Make coqdep find Require commands prefixed by Time
Support for Timeout n and From ..

- The state machine gets kind of complex
  maybe it should become a parser at some point?
a comment about the new state.
coqdep comments counter is in the stack
factored out require_modifiers + bug fix.

Conflicts:
	tools/coqdep_lexer.mll
Correct a spelling mistake
Grammar: "allowing to" is not proper English

I'm not quite sure why, but I'm pretty sure it's not.  Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".

I haven't touched the older instances of it in the CHANGES file.