Using IStream coiterator to explicit the captured state of tactic matching results.
In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in MathClasses).
Missing check of evar instantiation, resulting in missing constraints (bug from MathClasses).
In flex-flex cases, the undefinedness of an evar can not be preseved after converting
the stacks. Take care of this by recalling unification.
Coq_makefile: fix cmx compilation when there are both ml and mllib
Fix g_coqast for explicit applications.
Updating README wrt coq-club and ftp.
time tac
Revert "time tac" (committed by mistake).

This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
Exporting Proof.split in proofview.
Fixing bug #3270. Patch by Robbert Krebbers.
Recovering transparent state from kernel oracles in constant time.
Fixing the previous patch to keep transparent states in sync.
Arith: full integration of the "Numbers" modular framework

 - The earlier proof-of-concept file NPeano (which instantiates
   the "Numbers" framework for nat) becomes now the entry point
   in the Arith lib, and gets renamed PeanoNat. It still provides
   an inner module "Nat" which sums up everything about type nat
   (functions, predicates and properties of them).
   This inner module Nat is usable as soon as you Require Import Arith,
   or just Arith_base, or simply PeanoNat.

 - Definitions of operations over type nat are now grouped in a new
   file Init/Nat.v. This file is meant to be used without "Import",
   hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
   starts (but no proofs about them).

 - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
   are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
   where here Nat is Init/Nat.v).

 - This Coq.Init.Nat module (with only pure definitions) is Include'd
   in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
   sometimes instead of just Nat (for instance when doing "Print plus").
   Normally it should be ok to just ignore these "Init" since
   Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
   it's possible to get rid of these "Init" prefixes.

 - Concerning predicates, orders le and lt are still defined in Init/Peano.v,
   with their notations "<=" and "<". Properties in PeanoNat.Nat directly
   refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
   also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
   we cannot yet include an Inductive to implement a Parameter), but these
   aliased predicates won't probably be very convenient to use.

 - Technical remark: I've split the previous property functor NProp in
   two parts (NBasicProp and NExtraProp), it helps a lot for building
   PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:

   Module Nat.
     Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
     ... (** proofs of specifications for basic ops such as + * - *)
     Include NBasicProp. (** generic properties of these basic ops *)
     ... (** proofs of specifications for advanced ops (pow sqrt log2...)
             that may rely on proofs for + * - *)
     Include NExtraProp. (** all remaining properties *)
   End Nat.

- All other files in directory Arith are now taking advantage of PeanoNat :
  they are now filled with compatibility notations (when earlier lemmas
  have exact counterpart in the Nat module) or lemmas with one-line proofs
  based on the Nat module. All hints for database "arith" remain declared
  in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
  files are still Require'd (or not) by Arith.v, just as before.

- Compatibility should be almost complete. For instance in the stdlib,
  the only adaptations were due to .ml code referring to some Coq constant
  name such as Coq.Init.Peano.pred, which doesn't live well with the
  new compatibility notations.
Locate: also display some information about module aliasing

 Typically, if module M has a constant t and module P contains "Include M",
 then "Locate t" will now mention that P.t is an alias of M.t
Revert patch making the oracle be used for the transparent state in evarconv,
which made CoRN (and probably Ergo) fail. Another option should be found for
making a constant not unfoldable by tactics/refinement.
Fix a oversight in 5bf9e67b .

About 8 months after making this commit, I realised that I forgot to change a tclORELSE into a tclOR (which was the whole point of the commit to begin with). Shame on me.

It does not seem to have much of an effect on efficiency, though. It may be a hair faster, but mostly indistinguishably so.
Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).
check_for_interrupt: better (but slower) in threading mode

Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.
more APIs in TQueue and CThread

These are now sufficient to implement PIDE