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}.