Merge pull request #647 from eponier/local-scope

[derive] Open scope only locally
LPCIC · Jul 2, 2024 · 55e6039 · 55e6039
2 parents 1fbc593 + 934694f
commit 55e6039
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/apps/derive/theories/derive/eqb_core_defs.v b/apps/derive/theories/derive/eqb_core_defs.v
@@ -5,7 +5,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Open Scope positive_scope.
+Local Open Scope positive_scope.
 
 Section Section.
 Context {A:Type}.