Use a standard way to encode license names in packages

[palmskog]

The names of licenses in packages appears to currently be subject to informal conventions (albeit quite uniform such conventions). For example, grepping in released repo recently revealed:

• 277 opam files with LGPL in the license field
• 198 of those entries match LGPL 2, 20 match LGPL 3, 56 match LGPL\"

While there are thus only a few packages that use "LGPL" in a completely unconventional way, all of the above entries are actually ambiguous. A formal license name encoding such as SPDX reveals that, for example, LGPL 2.1 can mean LGPL-2.1-only or LGPL-2.1-or-later, which have very different legal consequences.

Adopting SPDX (or another similar formal scheme) for the Coq OPAM archive would not only make licenses unambiguous, but also make it possible to check packages in CI for license compliance with respect to their dependencies.

Thanks to @Zimmi48 who highlighted SPDX in a recent discussion in Coq-community, and who also successfully suggested it for adoption for Elm packages.

Arguably, SPDX could even be adopted at the global OPAM repository level, but this archive could be a good showcase to convince upstream OPAM maintainers.

[palmskog]

It seems that the official OPAM repo recently did a big SPDX conversion. However, this resulted in several erroneous license identifiers, as discussed in ejgallego/coq-serapi#185. It may still be worth doing a similar conversion here.