rm .classical

classical/all_classical.v

@@ -1,7 +1,7 @@
-From mathcomp.classical Require Export boolp.
-From mathcomp.classical Require Export classical_sets.
-From mathcomp.classical Require Export mathcomp_extra.
-From mathcomp.classical Require Export functions.
-From mathcomp.classical Require Export cardinality.
-From mathcomp.classical Require Export fsbigop.
-From mathcomp.classical Require Export set_interval.
+From mathcomp Require Export boolp.
+From mathcomp Require Export classical_sets.
+From mathcomp Require Export mathcomp_extra.
+From mathcomp Require Export functions.
+From mathcomp Require Export cardinality.
+From mathcomp Require Export fsbigop.
+From mathcomp Require Export set_interval.

classical/cardinality.v

@@ -1,8 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 
 (******************************************************************************)
 (*                              Cardinality                                   *)

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.
-From mathcomp.classical Require Import mathcomp_extra boolp.
+From mathcomp Require Import mathcomp_extra boolp.
 
 (******************************************************************************)
 (* This file develops a basic theory of sets and types equipped with a        *)

classical/fsbigop.v

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

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.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".

classical/set_interval.v

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

theories/Rstruct.v

@@ -372,7 +372,7 @@ Canonical R_rcfType := RcfType R Rreal_closed_axiom.
 End ssreal_struct.
 
 Local Open Scope ring_scope.
-From mathcomp.classical Require Import boolp classical_sets.
+From mathcomp Require Import boolp classical_sets.
 Require Import reals.
 
 Section ssreal_struct_contd.

theories/charge.v

@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets cardinality.
-From mathcomp.classical Require Import mathcomp_extra functions fsbigop.
-From mathcomp.classical Require Import set_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality.
+From mathcomp Require Import functions fsbigop set_interval.
 From HB Require Import structures.
 Require Import reals ereal signed topology numfun normedtype sequences.
 Require Import esum measure realfun lebesgue_measure lebesgue_integral.

theories/constructive_ereal.v

@@ -10,7 +10,7 @@
    incorporate it into mathcomp proper where it could then be used for
    bounds of intervals*)
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra.
 Require Import signed.
 
 (******************************************************************************)

theories/convex.v

@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets set_interval.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
-Require Import ereal reals signed topology prodnormedzmodule.
-Require Import normedtype derive realfun itv.
+From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
+From mathcomp Require Import functions cardinality.
+Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
+Require Import realfun itv.
 From HB Require Import structures.
 
 (******************************************************************************)

theories/derive.v

@@ -1,7 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
 
 (******************************************************************************)

theories/ereal.v

@@ -6,8 +6,8 @@
 (* -------------------------------------------------------------------- *)
 
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import boolp classical_sets functions fsbigop.
-From mathcomp.classical Require Import cardinality set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import fsbigop cardinality set_interval.
 Require Import reals signed topology.
 Require Export constructive_ereal.
 

theories/esum.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology sequences normedtype numfun.
 
 (******************************************************************************)

theories/exp.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import mathcomp_extra.
 Require Import reals ereal nsatz_realtype.
 Require Import signed topology normedtype landau sequences derive realfun.
 Require Import itv convex.

theories/itv.v

@@ -2,7 +2,7 @@
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
 From mathcomp Require Import interval.
-From mathcomp.classical Require Import boolp mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp.
 Require Import signed.
 
 (******************************************************************************)

theories/kernel.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality fsbigop.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import numfun lebesgue_measure lebesgue_integral.
 

theories/landau.v

@@ -1,7 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import ereal reals signed topology normedtype prodnormedzmodule.
 
 (******************************************************************************)

theories/lebesgue_integral.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop .
 Require Import signed reals ereal topology normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun.
 

theories/lebesgue_measure.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology numfun normedtype.
 From HB Require Import structures.
 Require Import sequences esum measure real_interval realfun exp.
@@ -2103,4 +2103,4 @@ exists (B `|` C); split.
 - by rewrite setUC -setDDl. 
 Qed.
 
-End egorov.
+End egorov.

theories/measure.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop .
 Require Import reals ereal signed topology normedtype sequences esum numfun.
 From HB Require Import structures.
 

theories/normedtype.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality set_interval.
 Require Import ereal reals signed topology prodnormedzmodule.
 
 (******************************************************************************)

theories/nsatz_realtype.v

@@ -1,6 +1,6 @@
 Require Import Nsatz.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
-From mathcomp.classical Require Import boolp.
+From mathcomp Require Import boolp.
 Require Import reals ereal.
 
 (******************************************************************************)

theories/numfun.v

@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
-From mathcomp Require Import ssralg ssrnum ssrint interval finmap.
-From mathcomp.classical Require Import boolp classical_sets fsbigop.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop.
+From mathcomp Require Import functions cardinality .
 Require Import signed reals ereal topology normedtype sequences.
 
 (******************************************************************************)

theories/probability.v

@@ -1,8 +1,8 @@
 (* 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.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
 From HB Require Import structures.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import exp numfun lebesgue_measure lebesgue_integral.

theories/real_interval.v

@@ -1,9 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
-From mathcomp.classical Require Export set_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Export set_interval.
 From HB Require Import structures.
 Require Import reals ereal signed topology normedtype sequences.
 

theories/realfun.v

@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
-From mathcomp.classical Require Import boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality mathcomp_extra.
-Require Import ereal reals signed topology prodnormedzmodule.
-Require Import normedtype derive real_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
+Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
+Require Import real_interval.
 From HB Require Import structures.
 
 (******************************************************************************)

theories/reals.v

@@ -36,8 +36,7 @@
 (******************************************************************************)
 
 From mathcomp Require Import all_ssreflect all_algebra.
-From mathcomp.classical Require Import boolp classical_sets set_interval.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
 
 Require Import Setoid.
 

theories/sequences.v

@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
-From mathcomp.classical Require Import boolp classical_sets.
-From mathcomp.classical Require Import functions set_interval mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import set_interval.
 Require Import reals ereal signed topology normedtype landau.
 
 (******************************************************************************)

theories/signed.v

@@ -1,7 +1,7 @@
 (* 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.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra.
 
 (******************************************************************************)
 (* This file develops tools to make the manipulation of numbers with a known  *)

theories/summability.v

@@ -2,9 +2,8 @@
 Require Reals.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import interval zmodp.
-From mathcomp.classical Require Import boolp classical_sets.
-Require Import ereal reals.
-Require Import Rstruct signed topology normedtype.
+From mathcomp Require Import boolp classical_sets.
+Require Import ereal reals Rstruct signed topology normedtype.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/topology.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import cardinality mathcomp_extra fsbigop.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import cardinality mathcomp_extra fsbigop.
 Require Import reals signed.
 
 (******************************************************************************)

theories/trigo.v

@@ -1,8 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
-From mathcomp.classical Require Import boolp classical_sets functions.
-From mathcomp.classical Require Import mathcomp_extra.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals ereal nsatz_realtype signed topology normedtype landau.
 Require Import sequences derive realfun exp.