From 46e8f68d0322e492d5b241d7014e65394a5d1843 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Sep 2023 17:02:12 +0200
Subject: [PATCH] enable name mangling

---
 iris/prelude/options.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/iris/prelude/options.v b/iris/prelude/options.v
index d7a84d1c1..d63c30ddf 100644
--- a/iris/prelude/options.v
+++ b/iris/prelude/options.v
@@ -16,6 +16,11 @@ From stdpp Require Export options.
 that at least global hints are annotated. *)
 #[export] Set Warnings "+deprecated-hint-without-locality".
 
+#[export] Set Mangle Names.
+#[export] Set Mangle Names Light.
+(** Make these names stand out more, in case one does end up in the proof script. *)
+#[export] Set Mangle Names Prefix "__".
+
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
 From iris.prelude Require Import options.
-- 
GitLab