Move to coq main line / relicensing

[MSoegtropIMC]

As discussed in coq-community/manifesto#163 (see there for further references) it would make sense to integrate this plugin into the main line. This has been discussed in the recent Coq call 2024-10-29 and the Coq developer team is positive about this.

A not necessarily required but convenient step would be to relicense this to the license of Coq (LGPL-2.1 only). It likely makes sense to dual license it.

What do the contributors think of both, the move and the relicensing?

@liyishuai @JasonGross @SkySkimmer @herbelin @Zimmi48 @gares

Please state your agreement to the move and the relicensing here (preferably state your opinion on both variants, a dual license and a single new license).

[JasonGross]

I'm in favor of the move. I never understood why this was a separate repo in the first place.

I have no opinion on relicensing vs dual licensing, and am happy to do whatever is most convenient

[MSoegtropIMC]

A note on the license: as discussed in Zulip the preferred option is to archive the repo here using the current license and use the new license only for the copy living in the Coq repo then.

[liyishuai]

A note on the license: as discussed in Zulip the preferred option is to archive the repo here using the current license and use the new license only for the copy living in the Coq repo then.

I second this archiving and relicensing plan.

[SkySkimmer]

all ok

[gares]

I'm in favor of the move to the coq repo.
I'm in favor of relicensing the code under the same license of Coq (LGPL 2.1 only).

[herbelin]

All ok, I'm following the (meta)move for a move. I a priori favor a relicensing the code under the same license of Coq.