Set officially the minimal OCaml requirement to 3.12.1

 Anyway, a few syntactic features of 3.12 were already used here and
 there (e.g. local opening via Foo.(...), or the record shortcut
 { field; ... }). Hence compiling with 3.11 wasn't working anymore.

 Already take advantage of the following 3.12.1 features :
 - "module type of ..." in CArray, CList, CString ...
 - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
   via our coqdep to localize the .ml4 modules :-)

 The -ml-synonym option (+ various bugfixes) is the reason for asking
 3.12.1 directly and not just 3.12.0. After all, if debian stable is
 providing 3.12.1, then everybody has it ;-)
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)

 There are currently two other clashs : Lexer and Errors, but for
 the moment these ones haven't impacted my experiments with extraction
 and compiler-libs, while this Matching issue had. And anyway the new
 name is more descriptive, in the spirit of the recent TacticMatching.
Fixing generic hashes and replacing them with proper ones.
Replacing arguments of Trie by a cancellable monoid.
Extruding code not depending of the functor argument in Termdn.
Removing Termdn, and putting the relevant code in Btermdn. The current Termdn
file was useless and duplicated code from Btermdn itself.
Term dnets do no need to contain the afferent constr pattern in their nodes.
Goptions do not rely anymore on generic equality.
Kernel names are implemented using records.
Getting rid of generic hashes in cc plugin.
Removing generic hashes in kernel.
Fixing pervasive equalities. In particular, I removed the code that deleted
duplicates in kernel side effects. They were chosen according to an equality
that was quite irrelevant, and as expected this patch did not break the
test-suite.
Fixing Pervasives.equality in extraction.
Fixing some generic equalities in Micromega.
STM: when finish a task hcons universe constraints
STM: fix Show Script
Move error and job display to the lower right pane.
Fixing pervasives equalities in Vconv.
Adding a CSet module in Coq lib.
Correct handling of hashconsing of constraint sets. The previous implementation
did not respect the requirement that equality should preserve hash.