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.
Printing heap on every processed sentence.

git-svn-id: https://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
Profile only when CAMLRUNPARAM is set.

git-svn-id: https://scm.gforge.inria.fr/svn/coq/trunk@16950 85f007b7-540e-0410-9357-904b9bb8a0f7
Better interface for allocation profiling.
Exporting print_heap in Vernac.
Adding a tactic to dump major heap.