Merge PR #11368: Turn trailing implicit warning into an error

Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes

1 files changed, 33 insertions, 0 deletions

diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
new file mode 100644
index 0000000000..a125337dd9
--- /dev/null
+++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
@@ -0,0 +1,33 @@
+if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then
+
+    mathcomp_CI_REF=non_maximal_implicit
+    mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp
+
+    oddorder_CI_REF=non_maximal_implicit
+    oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order
+
+    stdlib2_CI_REF=non_maximal_implicit
+    stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2
+
+    coq_dpdgraph_CI_REF=non_maximal_implicit
+    coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph
+
+    vst_CI_REF=non_maximal_implicit
+    vst_CI_GITURL=https://github.com/SimonBoulier/VST
+
+    equations_CI_REF=non_maximal_implicit
+    equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations
+
+    mtac2_CI_REF=non_maximal_implicit
+    mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2
+
+    relation_algebra_CI_REF=non_maximal_implicit
+    relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra
+
+    fiat_parsers_CI_REF=non_maximal_implicit
+    fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat
+
+    Corn_CI_REF=non_maximal_implicit
+    Corn_CI_GITURL=https://github.com/SimonBoulier/corn
+
+fi