math-comp · hoheinzollern · May 12, 2025
diff --git a/Makefile.coq.local b/Makefile.coq.local
diff --git a/experimental_reals/Makefile.coq.local b/experimental_reals/Makefile.coq.local
diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v
@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

diff --git a/reals/Makefile.coq.local b/reals/Makefile.coq.local
diff --git a/reals/reals.v b/reals/reals.v
@@ -38,7 +38,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Corelib Require Import Setoid.
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.