bump min version to 8.19

[Alizter]

We bump our minimal Coq version to 8.19.

This version appears to have some better universe inference and will be useful for #1984.

I did a compatibility cleanup in No/Core.v.

I noticed that there is an 8.19 compatibility comment in Quotient.v but I couldn't work out what exactly could change. @jdchristensen would you mind taking a look at that file and dropping the 8.18 compat? (Alternatively, we can do that in a later PR it doesn't seem too pressing).

The draft PR #1862 can be undrafted after this.

[jdchristensen]

I did a compatibility cleanup in No/Core.v.

Did you forget to include this? Do you want me to push changes to Quotient.v to this PR?

[Alizter]

@jdchristensen Just forgot to push. You can go ahead and push changes to Quotient.v here.

[jdchristensen]

@Alizter This LGTM, but I don't know why the CI isn't running for my latest commit.

[jdchristensen]

Ok, the CI is running now, but one of the nix jobs is still at 8.18.

[jdchristensen]

I tried changing an "8.18" to "8.19" in flake.nix, but the build still seems to be using 8.18. I don't know anything about nix, so I'll leave this to @Alizter .

[Alizter]

@jdchristensen Yes, I forgot to change that. There was a new version of coq-lsp released so I'd lile to wait a tad longer before updating the nix stuff.

[Alizter]

I've updated the nix flake to a version that includes the latest coq-lsp which was released this week. The issue from before was because the Nix flake's lockfile was not updated, which can be done by nix flake check or nix develop. And since we are updating the lockfile I decided we might as well bump to the latest available packages.

This is now ready to be merged if you are fine with it @jdchristensen.

[Alizter]

I noticed you wrote LGTM before so I will take this as a green light and proceed.