From 419e46bd283f206930d3ad7603758cecc01bb84f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 May 2021 11:32:20 +0200
Subject: [PATCH] remove unnecessary 'Open Scope'
---
iris/proofmode/string_ident.v | 2 --
1 file changed, 2 deletions(-)
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 6143cefe5..6bdb66392 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -77,8 +77,6 @@ Module StringToIdent.
intros $ident).
End StringToIdent.
-Global Open Scope string_scope.
-
(** Finally we wrap everything up intro a tactic that renames a variable given
by ident [id] into the name given by string [s].
Only works if [id] can be reverted, i.e. if nothing else depends on it. *)
--
GitLab