Adding a coiterator to IStream.
coqdoc is minimaly -Q aware
Fix Coq_makefile in presence of mlpack
Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
Restore proper order of effects in letin_tac_gen. Fixes CFGV again.
Properly compute the transitive closure of the system of constraints
generated by a mutual inductive definition (bug found in CFGV). Actually this
code can move out of the kernel.
Cleanup code related to the constraint solving, which sits now outside the
kernel in library/universes.ml.
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.
Rewritten the tactic monad in plain ML. It uses second-order typing thanks to
records.