Extend the test suite (with coq 8.12.1 and coq-native)

* Follow-up of math-comp@52988b6

* Now possible after the merge of rocq-prover/opam#1835

Author: erikmd

.github/workflows/ci.yml

@@ -35,9 +35,7 @@ jobs:
               . configure  # sourcing mandatory
               coq_version
             endGroup
-            # Note: Replace with "if coq_native_compiler"
-            # to also test with Coq 8.12.1+
-            if coq_native_compiler_default; then
+            if coq_native_compiler; then
               startGroup "Workaround permission issue"
                 sudo chown -R coq:coq .  # <--(§)
               endGroup

configure

@@ -36,9 +36,7 @@ coq_native_compiler() {
 }
 
 main() {
-    # Note: Replace with "if coq_native_compiler"
-    # to also test with Coq 8.12.1+
-    if coq_native_compiler_default; then
+    if coq_native_compiler; then
         echo 'coq-native support enabled!' >&2
         sed -e 's/;coq-native-disabled; \?//' "$dir/src/dune.in" > "$dir/src/dune"
     else