Merge branch 'robbert/no_native_compute' into 'master'

Avoid relying on native_compute.

See merge request iris/iris!865

_CoqProject

@@ -10,6 +10,8 @@
 -Q iris_heap_lang iris.heap_lang
 -Q iris_unstable iris.unstable
 -Q iris_deprecated iris.deprecated
+# Avoid needlessly increasing our trusted code base with native_compute
+-arg -native-compiler -arg no
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures