It might be useful to have support for Rocq 9.0. Rocq 9 is quite different from 8.20, so we might want two options for the hs-to-coq program so that we can choose to export to Coq 8.20 or Rocq 9.0. We can keep all examples (esp. large ones with convenience copies) at Coq 8.20; but we might be able to test examples/tests in both versions of Rocq/Coq?
It might be useful to have support for Rocq 9.0. Rocq 9 is quite different from 8.20, so we might want two options for the hs-to-coq program so that we can choose to export to Coq 8.20 or Rocq 9.0. We can keep all examples (esp. large ones with convenience copies) at Coq 8.20; but we might be able to test examples/tests in both versions of Rocq/Coq?