Generalize EqdepFacts

The generalized versions are names *_one_var.  We preserve backwards
compatibility by defining the old versions in terms of the generalized
ones.

This closes the rest of Bug 3019, and closes pull request #6.
sed s'/_one_var/_on/g'

For consistency with ChoiceFacts
Debug RAKAM
Configure.ml creates metadata to annotate MacOS binaries
Distributed binaries under MacOS are signed.
Add t-jagro to .mailmap
Prove forall extensionality
Add a regression test for 3427
Fixing bug #3493.

Coq now accepts the [Universes u1 ... un] syntax.
Removing spurious tclWITHHOLES.

Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.
Protect against "it's unifiable, if you solve some unsolvable constraints" behavior of evar_conv_x,
getting more common after patch on evars and eta. The main problem is that ?X = C[?X] problems get
postponed now, when they failed earlier before (rendering the algorithm incomplete, e.g. on ?X = \y. ?X y).
A notion of "rigid/strongly rigid" occurrences would give a better fix.
Fixing bug #3541.

All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
Adding test-suite for bug #3212.
Cleaning and documenting a bit the Proofview.Refine module.
Fixing an unnatural selection of subterms larger than expected in the
presence of let-ins.