This is in preparation for coq/coq#9274.

This lemma allows one to get the witness out of a later, without having
to use `later_car`, i.e. in a way that works in the on-paper version of
the logic.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

Added a new lemma to allocate fragmented ownership in unital gmaps while updating the full ownership

These results turned out to be neither that useful nor canonical, and can easily
be derived from local updates.

This reverts commit 465dd9f4.

Thanks to @jung for proposing these names.

`sed -i 's/frag_auth_op/frac_auth_frag_op/g' $(find -name "*.v")`

This is backwards-compatible; it desugars to a normal application on previous versions

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type."

This reverts commit fa897ff5.

The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.