test-suite: opaque term -> opaque proof
Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infinite loop.
Pos.compare_cont takes the comparison as first argument

Helps cbn tactic refolding
Removing a Pervasives.compare in Term_dnet.
Removing Pervasives.compare in Termdn.
Removing a fishy use of pervasive equality in Ltac backtrace printing.
Hunting pervasive equality in native compiler. It seems they were used for
optimization purposes. I replaced their use with the under-approximation
of pointer equality.
Useless check when loading notations through import.
Fixing bad comparison in Detyping.
Never suppress the typing constraint of bound variables whose name was
reserved with Implicit Type.
Better behaviour for sets of reserved names.
Fixing pervasive comparisons
Fix syntax highlighting of "Implicit Arguments" for gtksourceview.
Fixing generic Hashtbl.hash in Constr.
Adding an equality function over glob_constr
Removing generic equality in Syntax plugin.
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code

 NB: new file miscprint.ml deserves to be part of printing.cma,
 but should be part of proofs.cma for the moment, due to use in logic.ml
Migrate back g_obligations in toplevel

 This almost reverts commit 845d6f (r15248).

 It isn't ideal to put syntactic stuff in the toplevel directory.
 Maybe this kind of files should have someday their own directory
 along with g_rewrite.ml4 and some other (maybe a extraparsing dir?).

 Meanwhile, this commit leads to a cleaner situation concerning *.ml4:

 - everything needed to build grammar.cma (and q_constr.cmo) is in:
   lib/ kernel/ library/ pretyping/ interp/ proofs/ parsing/ grammar/

 - all *.ml4 using grammar.cma (or q_constr.cmo) are in:
   tactics/ toplevel/ plugins/*/
Makefile: the initial build of grammar.cma is now directory-driven

 In last commit, we used grep to decide whether a .ml4 could be
 compiled during the initial phase of not. Instead, we now rely on
 a simpler directory dichotomy:

 - config lib kernel library pretyping interp parsing grammar
   are considered initial (and shouldn't contain grammar-dependent .ml4),
   see $(GRAMSRCDIRS) in Makefile.common

 - the grammar-dependent .ml4 could be in any other directories
   Currently, they are in: tactics toplevel plugins/*
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 ;-)