From 934694f1acec7da2087283e2500151250dfb4591 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Christophe=20L=C3=A9chenet?= Date: Tue, 2 Jul 2024 15:00:46 +0200 Subject: [PATCH] [derive] Open scope only locally --- apps/derive/theories/derive/eqb_core_defs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/derive/theories/derive/eqb_core_defs.v b/apps/derive/theories/derive/eqb_core_defs.v index c6fb6e185..a02c89081 100644 --- 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}.