Apply the patch "inductive-indice-levels-matter-8.3.patch" from Hugo Herbelin.

    As Voevodsky says:

       Hugo's patches "inductive-indice-levels-matter-8.3.patch" and
       "patch.type-in-type" are intended only as a temporary solution for the universe
       management issues in Coq which arise in connection with the univalent approach.

       The first of these patches changes the way the universe level of inductive
       types is computed for those definitions which do not specify [ Set ] or [ Prop
       ] as the target of the inductive construction explicitely. The new computation
       rule for the universe level takes into account not only the u-levels of the
       types occuring in the constructors but also the u-levels of types occuring in
       "pseudo-parametrs" i.e. in the [ forall ] expressions in the type of the
       inductive definition. For example, in the definition:

         [ Inductive Ind ( a1 : A1 ) : forall a2 : A2 , Type := ... ]

       The u-level of [ Ind ] will be the maximum of the u-level computed on the basis
       of types occuring in the constructors and the u-level of [ A2 ]. The u-level of
       [ A1 ] which the type of a parameter [ a1 ] ( as opposed to a pseudo-parameter
       [ a2 ] ) is not taken into account.
    Apply the patch "patch.type-in-type" from Hugo Herbelin.

    As Voevodsky says, "Hugo's patches "inductive-indice-levels-matter-8.3.patch"
    and "patch.type-in-type" are intended only as a temporary solution for the
    universe management issues in Coq which arise in connection with the univalent
    approach."

    This patch is the second of those: "The second patch switches off the universe
    consistency checking in Coq which is a temporary measure which allows us to
    formalize interesting constructions such as [ ishinh ] and [ setquot ] without
    having the resizing rules."
    Apply Grayson's patch "fix-hanging-at-end-of-proof.patch"

    This patch turns off the "sharing" flag.

    As Voevodsky says:

        The patch uses a flag previously installed in the source code to switch off
        some optimization features of the algorthim. The need for this patch has arised
        because of several cases when Coq process would hang after "Admitted". In
        practice the patch prevents hangings but makes compilation of some of the code
        slower. In particular, with this patch installed the current standard library
        file Cycllic31.v does not compile in a reasonable amount of time (see the
        suggestion of how to compile Coq without much of the standard library
        below). It also affect the time of compilation for some of the "computation
        tests" in the Foundations library increasing the compilation time by a factor
        of >5. Hopefully, the actuall buf will be located and removed in the next
        update.

    Grayson's guess about the problem:

        When reducing a term to normal form, it may happen that a subexpression,
        upon which you've spent much time to reduce it, is ultimately discarded and
        not incorporated into the answer; think of a function that ignores one of
        its variables. So, to save time, don't reduce a subexpression until you
        have to.  To do that, you have to distinguish terms that have been reduced
        from terms that need to be reduced.  All of that is the laziness aspect.
        Now for the sharing; if a subexpression appears twice in the term, then you
        would like to reduce it just once, so the subexpression should be
        modifiable so that after reduction, you can replace it in place
        (destructively) by its reduced form. That's the sharing aspect.  But
        destructive modification of data structures can easily lead to bugs.
        That's why ocaml code that uses them has explanation points (!) or
        colon-equal signs (:=) in it, so your eye is attracted to them.  In the
        debugger, the execution of your hung-up "Defined" proceeded deeper and
        deeper without making progress, always passing the same use of destructive
        modification, so it was natural to suspect a problem.
    Apply Grayson's patch "grayson-fix-infinite-loop.patch"

    This "fixes" a seemingly infinite loop by abandoning the routine after ten repetitions.
    A better fix would involve understanding what the code was supposed to do.
apply patch "grayson-improved-abstraction-version2-8.3pl2.patch"

As Voevodsky says:

   This patch dramatically improves the behavior of the [destruct] tactic making
   it applicable in many the cases when dependencies are present. It is not
   creating any complicated proof terms but simply uses the eliminator for
   inductive definitions in a more intelligent way than the standard [ destruct ].
Apply Grayson's patch "grayson-closedir-after-opendir.patch"

It improves the management of file openings/closing and eliminates in most
cases the complaint that there are too many open files.