From 93d9ef74618c4d252c200f2f1ff4ac433c034a1f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Nov 2022 13:23:29 +0100
Subject: [PATCH] Avoid relying on native_compute.

---
 _CoqProject | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/_CoqProject b/_CoqProject
index 198cf2a91..6f4e56950 100644
--- a/_CoqProject
+++ b/_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
-- 
GitLab