I'm able to perform an `Import Order.NatOrder.`

, but this doesn't seem to work with `Import Order.OrdinalOrder.`

Is this because I'm still using Coq/ssreflect/mathcomp 8.13? I didn't manage to locate the log for changes.

it seems lots of things have been added to `order.v`

in 1.13. (see changelog). Which version of mathcomp are you using?

Thanks for the log URL. My `default.nix`

file mentions `pkgs.coqPackages_8_13.mathcomp`

. What would be the best way to test the version this corresponds to?

Pierre Jouvelot said:

Thanks for the log URL. My

`default.nix`

file mentions`pkgs.coqPackages_8_13.mathcomp`

. What would be the best way to test the version this corresponds to?

Haha, I see that `Print LoadPath`

mentions a `mathcomp-all-1.12.0`

!

Now, I just need to upgrade my nix installation to support 1.13. Any suggestion on how to do this as painlessly as possible? ;)

switch to opam, or use the Coq Nix toolbox? https://github.com/coq-community/coq-nix-toolbox

I'm already using nix, which I find really convenient on my Mac. I'll look at the toolbox to see how I can do the upgrade, then. Thanks.

Last updated: Feb 08 2023 at 04:04 UTC