It has been accidentaly broken since early 2014 (and especially
 in 8.5), no easy repair, I won't devote any more hours to this stuff.
 Moreover no one seems to care apart from Emilio, but he's ok to work
 on this in a separate repository or branch.
 I left a dev/doc/ocamlbuild.txt file with a few words about this
 experiment.

This patch splits pretty printing representation from IO operations.

- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.

The patch continues work initiated for 8.5 and has the following effects:

- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
  `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
  `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
  used instead.

- Feedback provides different backends to handle output, currently,
  `stdout`, `emacs` and CoqIDE backends are provided.

- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
  gone.

- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
  mix.

Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.

together with the tactic monad.

The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.

Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.

 * vars.mli was mentionning Term instead of Constr, leading to a dep cycle
 * Having a file named toplevel/toplevel.ml isn't a good idea when we also
   have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
   We rename toplevel.ml into Coqloop.ml
 * Extra cleanup of toplevel.mllib :
   - Ppextra isn't anywhere around (?!)
   - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
   - Vernacexpr is a .mli and shouldn't appear in an .mllib
 * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
 * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
   for coqchk).

 No need to place these binaries apart, and anyway they aren't
 (shell) scripts since ages.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7

Preparing landing of the native compiler, which requires -rectypes flag.

This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7

 Threads were only there to handle blocking dialogs with the different
 coqtops. But programming with threads have drawbacks : complex mutex
 infrastructure, possible deadlocks, etc. In particular gtk functions
 are not meant to be called from a thread which isn't the gtk main loop,
 (unless some gtk mutex have been taken). This seem to pose problem
 specifically in win32 (and macosx ?), hence the use of the
 GtkThread.(a)sync hack for scheduling code for execution in the gtk
 main loop.

 Instead, we now use the Glib.Io module to install a callback that will
 be runned when some answer of coqtop is available on the channel.
 This implies using now a continuation-passing style: for instance,
 instead of two sequential requests to coqtop, we'll now have the
 2nd request inside the callback handling the answer to the 1st request.

 Remarks:

 - Also use asynchronous i/o for external commands (editor, coqc, make...).
   Launching an external editor or browser won't freeze coqide anymore.

 - Reworked handling of coqtop process, especially when closing them.
   A responsive coqtop should now hara-kiri immediatly when its input
   channel is closed. Otherwise we try later a soft kill, then some
   hard kills if necessary. If nothing work we warns the user.
   When quitting coqide, all this might induce a small delay (2s at worse).

 - Be careful now to avoid "long" computations (or blocking i/o) in
   a coqide function. Experimentally, it seems that loading/saving a .v
   file is quick enough. If necessary, we could use asynchronous i/o
   also for writing the .v, but for loading I've no clue.

 - In the Coqide module, we ensure that the current continuation k
   will indeed be run at the end thanks to an abstract return type
   (void = opaque copy of unit).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7

 The IFDEF's in mltop.ml4 were there to support platforms with
 a native ocaml compiler but no dynlink.cmxa, a situation that
 should be pretty rare in the Coq community nowadays (playing
 with coqtop on ARM, anyone ?). So we now refuse to build
 a native coqtop unless dynlink.cmxa exists (cf ./configure),
 and we explain how to create a dummy one if necessary
 (cf dev/dynlink.ml). This way, we can clean-up mltop.ml,
 and remove ugly special rules in Makefile and myocamlbuild

 NB: I checked that this shouldn't have any impact on Coq's
 debian packages on exotic architectures (arm, mips, ...),
 since apparently on these architectures no ocamlopt at all
 are shipped, and coq packages are already byte-only

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7