Resurrect the cofix transform, adding a new axiom for the admitted pr…

[mattam82]

…oofs.

Generalize MetaCoq Erase to take options allowing to optionally run this pass, a la CertiCoq.
This gives the following options:

Usage:
To erase a Gallina definition named <gid> type:
MetaCoq Erase <options> <gid>.

To show this help message type:
MetaCoq Erase -help.

Valid options:
-typed	   :  Run the typed erasure pipeline including a dearging phase. By default we run the pipeline without this phase.
-unsafe      :  Run also partially verified passes of the pipeline. This includes the cofix to fix translation.
-time        :  Time each compilation phase
-bypass-qeds :  Bypass the use of Qed and quote opaque proofs. Beware, this can result in large memory
consumption due to reification of large proof terms.
By default, we use the (trusted) Template-Coq quoting optimization that quotes every opaque term as an axiom.
All these axioms should live in Prop so that erasure is not affected by the absence of their bodies.
-fast        : Enables an alternative implementation of the parameter stripping phase that uses accumulators
instead of a view (see Erasure.ERemoveParams).

See https://metacoq.github.io for more detailed information.