Test case containing a proof of false due to a DeBruijn off-by-one error in the
code checking allowed sorts for elimination.
Christmas is over...
Implementing transitive reduction in the dependency graph printing
mechanism of coqdep.
Fixing bugs #1039: Hypotheses don't respect Barendregt convention
and #3204: Failure of hygiene condition.

It was sufficient to tweak a flag in the constr externalization...
Update .mailmap with recent contributors.

I should have updated everyone who committed since the migration to git (giving me a canonical email).

I've search git shortlog -s to ensure the best I could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed.
Fixing bug #1758: Print Hint output can be misleading if variable shadows hypothesis.
Follow-up of bugfix for #3204: local definitions were not handled properly.
Fixup make clean and .merlin
Makefiles use $(foo), not $foo, for variables

Also, we need :=, so that it's evaluated immediately, rather than
becoming a self-recursive variable.  This fixes the "Undefined variable
'C'" error that make keeps spewing.
Relaxing the sort elimination check to allow for let-bindings in arities.

I restored this in the kernel, and added it to the checker. There is one last
source of non-uniformity, which is the Sort case in the checker (was not
present in the kernel). I don't know what this case covers, so it should be
reviewed.
Fixing checker compilation, which was broken by the following commit:

05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
Fixing an interpretation bug with tactics in notations. For some obscure
reason, Ltac interpretation does not allow tactics of the following
shape : let x := bla in TacGeneric tac. Hence we force genargs to be
tactics and build the resulting hole tactic from scratch.
Adding a default object to generic argument registering mechanism.
Fixing coqdep graph printing. The transitive reduction algorithm was bugged.
Using full paths in coqdep -dumpgraph.
bug correction in proving principles of function
configure.ml fixed wrt Win32 + byte-only + coqide
Spawn: managed processes

The Spawn and Spawned modules factor the operation of spawning
a process.  Both synchronous and asynchronous channels are supported.
Both threaded and glib like main loop models are supported.  Still,
not all combinations are truly tested not equipped with a decent API:
only async + glib and sync + thread are, since these are the models we
use for coqide<->coqtop and coqtop<->worker respectively.
CoqIDE: ported to spawn
STM: ported to spawn