Merge pull request #118 from Villetaneuse/from_stdlib_warnings

Suppress 2 "From Stdlib" warnings
coq · Mar 10, 2025 · 6885eea · 6885eea
2 parents c33eae9 + ffef1ba
commit 6885eea
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/theories/Numbers/DecimalR.v b/theories/Numbers/DecimalR.v
@@ -14,7 +14,7 @@
     are bijections. *)
 
 From Stdlib Require Import Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions.
-Require Import PeanoNat.
+From Stdlib Require Import PeanoNat.
 
 Lemma of_IQmake_to_decimal num den :
   match IQmake_to_decimal num den with

diff --git a/theories/Reals/Zfloor.v b/theories/Reals/Zfloor.v
@@ -5,7 +5,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-Require Import Rbase Rfunctions Lra Lia.
+From Stdlib Require Import Rbase Rfunctions Lra Lia.
 
 Local Open Scope R_scope.