fix Scope

thery · thery · commit 871934b9d16a · 2025-01-23T15:23:30.000+01:00
diff --git a/theories/Reals/Zfloor.v b/theories/Reals/Zfloor.v
@@ -7,7 +7,7 @@
 
 Require Import Rbase Rfunctions Lra Lia.
 
-Open Scope R_scope.
+Local Open Scope R_scope.
 
 Definition Zfloor (x : R) := (up x - 1)%Z.
 
