Proofview.Notations: Now that (>>=) is free, use it for tclBIND.

Impacts MapleMode.
Remove unsafe code (Obj.magic) in Tacinterp.

This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
Code refactoring thanks to the new Monad module.
Tacinterp: refactoring using Monad.

Adds a combinator List.map_right which chains effects from right to left.
Tacinterp: more refactoring.

Introducing List.fold_right and List.fold_left in Monad.
better warning
amending last commit
Makefile: re-introduce 2 phases to avoid make strange -include's

Yet another revision of the build system. We avoid relying on the awkward
include-which-fails-but-works-finally-after-a-retry feature of gnu make.
This was working, but was quite hard to understand. Instead, we reuse
the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but
in a lighter way. The main Makefile calls Makefile.build twice :
 - first for building grammar.cma (and q_constr.cmo), with a restricted
   set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES).
 - then on the true target(s) asked by the user (using the special variable
   MAKECMDGOALS).

In pratice, this should change very little to the concrete developper's life,
let me know otherwise. A few more messages of make due to the explicit
first sub-call, but no more strange "not ready yet" messages...

Btw: we should handle correctly now the parallel compilation of multiple
targets (e.g. make -jX foo bar). As reported by Pierre B, this was
triggering earlier two separate sub-calls to Makefile.build, one
for foo, the other for bar, with possibly nasty interactions in case
of parallelism.

In addition, some cleanup of Makefile.build, removal of useless :: rules,
etc etc.
Fixing a Pervasive.compare.
Fix compilation of coq and plugins using coq_makefile under cygwin

Problems:
- strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config
  the value of "ranlinb" and replace ranlib by strip obtaining
  "i686-bla-strip" from "i686-bla-ranlib"
- coq_makefile was not quoting the plugins/ paths
- coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
.*.aux erased by make distclean
Dead code elimionation in reductionops
Fix output test-suite 'simpl tactic' -> 'reduction tactics'
test-suite: New names for vars but the expected invariant is preserved
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.