rebase

math-comp · Jun 6, 2023 · 30c1217 · 30c1217
1 parent 5cb5dec
commit 30c1217
Show file tree

Hide file tree

Showing 7 changed files with 14 additions and 11 deletions.
diff --git a/classical/cardinality.v b/classical/cardinality.v
@@ -2,7 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset.
-Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions.
 
 (******************************************************************************)
 (*                              Cardinality                                   *)

diff --git a/classical/classical_sets.v b/classical/classical_sets.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
 From mathcomp Require Import ssrint interval.
-Require Import mathcomp_extra boolp.
+From mathcomp.classical Require Import mathcomp_extra boolp.
 
 (******************************************************************************)
 (* This file develops a basic theory of sets and types equipped with a        *)

diff --git a/classical/fsbigop.v b/classical/fsbigop.v
@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-Require Import mathcomp_extra boolp classical_sets functions cardinality.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions cardinality.
 
 (******************************************************************************)
 (*                     Finitely-supported big operators                       *)

diff --git a/classical/functions.v b/classical/functions.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
-Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".

diff --git a/classical/set_interval.v b/classical/set_interval.v
@@ -1,7 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
+From mathcomp.classical Require Import functions.
 
 (******************************************************************************)
 (* This files contains lemmas about sets and intervals.                       *)

diff --git a/theories/itv.v b/theories/itv.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
-From mathcomp Require Import interval mathcomp_extra.
-From mathcomp.classical Require Import boolp.
+From mathcomp Require Import interval.
+From mathcomp.classical Require Import mathcomp_extra boolp.
 Require Import signed.
 
 (******************************************************************************)

diff --git a/theories/probability.v b/theories/probability.v
@@ -1,11 +1,11 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
-Require Import mathcomp_extra boolp reals ereal.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
-Require Import classical_sets signed functions topology normedtype cardinality.
-Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral.
-Require Import exp.
+From mathcomp.classical Require Import functions cardinality.
+Require Import reals ereal signed topology normedtype sequences exp esum.
+Require Import measure numfun lebesgue_measure lebesgue_integral.
 
 (******************************************************************************)
 (*                       Probability (experimental)                           *)