Skip to content

Commit e53316b

Browse files
LysxiaLysxia
authored
Merge pull request #208 from coq-community/stdlib_repo
Adapt to rocq-prover/rocq#19530
2 parents 7dc1ada + 823afcd commit e53316b

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

96 files changed

+251
-249
lines changed

‎algebra/CMonoids.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636

3737
(** printing [0] %\ensuremath{\mathbf0}% #0# *)
3838

39-
Require Export Coq.Arith.Euclid.
39+
From Coq Require Export Euclid.
4040
Require Export CoRN.model.Zmod.Cmod.
4141
Require Export CoRN.algebra.CSemiGroups.
4242
Require Export CoRN.tactics.csetoid_rewrite.

‎algebra/CRing_as_Ring.v

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11

2-
Require Export CoRN.algebra.CRings Coq.setoid_ring.Ring.
2+
Require Export CoRN.algebra.CRings.
3+
From Coq Require Export Ring.
34
Definition CRing_Ring(R:CRing):(ring_theory (@cm_unit R) (@cr_one R) (@csg_op R) (@cr_mult R) (fun x y => x [-] y) (@cg_inv R) (@cs_eq R)).
45
Proof.
56
split;algebra.

‎algebra/CSums.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@
4141
(** printing Sumx %\ensuremath{\sum'}% #∑'&*)
4242

4343
Require Export CoRN.algebra.CAbGroups.
44-
Require Export Coq.Arith.Peano_dec.
44+
From Coq Require Export Peano_dec.
4545
From Coq Require Import Lia.
4646

4747
(**

‎algebra/Expon.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636

3737
(** printing [^^] %\ensuremath{\hat{\ }}% #^# *)
3838

39-
Require Export Coq.Arith.Arith.
39+
From Coq Require Export Arith.
4040
Require Export CoRN.algebra.COrdCauchy.
4141
From Coq Require Import Lia.
4242

‎complex/NRootCC.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,8 @@
4040
(** printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
4141

4242
Require Export CoRN.complex.CComplex.
43-
Require Export Coq.Arith.Wf_nat.
44-
Require Export Coq.setoid_ring.ArithRing.
43+
From Coq Require Export Wf_nat.
44+
From Coq Require Export ArithRing.
4545
Import CRing_Homomorphisms.coercions.
4646

4747
(**

‎coq_reals/Rreals_iso.v

+11-11
Original file line numberDiff line numberDiff line change
@@ -17,22 +17,22 @@
1717
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
1818
*)
1919

20-
Require Import Coq.QArith.QArith.
21-
Require Import Coq.QArith.Qreals.
22-
Require Import Coq.QArith.QArith_base.
20+
From Coq Require Import QArith.
21+
From Coq Require Import Qreals.
22+
From Coq Require Import QArith_base.
2323
Require Import CoRN.tactics.CornTac.
24-
Require Import Coq.Reals.RIneq.
25-
Require Import Coq.Reals.Rcomplete.
26-
Require Import Coq.Reals.Rlimit.
27-
Require Import Coq.Reals.Rbasic_fun.
24+
From Coq Require Import RIneq.
25+
From Coq Require Import Rcomplete.
26+
From Coq Require Import Rlimit.
27+
From Coq Require Import Rbasic_fun.
2828
Require Import CoRN.coq_reals.Rreals.
2929
Require Import CoRN.reals.iso_CReals.
3030
Require Import CoRN.reals.CauchySeq.
31-
Require Import Coq.Reals.Rtrigo_def.
31+
From Coq Require Import Rtrigo_def.
3232
Require Import CoRN.transc.PowerSeries.
33-
Require Import Coq.Logic.ConstructiveEpsilon.
34-
Require Import Coq.Reals.Rlogic.
35-
Require Export Coq.Reals.Reals.
33+
From Coq Require Import ConstructiveEpsilon.
34+
From Coq Require Import Rlogic.
35+
From Coq Require Export Reals.
3636
Require Import CoRN.transc.Pi.
3737
Require Import CoRN.transc.MoreArcTan.
3838
Require Import CoRN.logic.PropDecid.

‎fta/KeyLemma.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,8 @@
3434
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
3535
*)
3636

37-
Require Export Coq.ZArith.ZArith.
38-
Require Export Coq.Arith.Compare.
37+
From Coq Require Export ZArith.
38+
From Coq Require Export Compare.
3939
Require Export CoRN.reals.NRootIR.
4040
From Coq Require Import Lia.
4141

‎ftc/WeakIVTQ.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Definition Q2R (q: Q) : IR := (inj_Q IR q).
77
Coercion Q2R : Q >-> st_car.
88

99

10-
Require Import Coq.setoid_ring.Ring.
10+
From Coq Require Import Ring.
1111
Require Import CoRN.tactics.CornTac.
1212
Require Import CoRN.algebra.CRing_as_Ring.
1313

‎logic/CLogic.v

+4-4
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,11 @@
4444
(** printing or %\ensuremath{\mathrel\vee}% *)
4545
(** printing and %\ensuremath{\mathrel\wedge}% *)
4646

47-
Require Export Coq.Arith.Compare_dec.
47+
From Coq Require Export Compare_dec.
4848
Require Export CoRN.logic.CornBasics.
49-
Require Export Coq.ZArith.ZArith.
50-
Require Export Coq.setoid_ring.ZArithRing.
51-
Require Export Coq.Arith.Wf_nat.
49+
From Coq Require Export ZArith.
50+
From Coq Require Export ZArithRing.
51+
From Coq Require Export Wf_nat.
5252
From Coq Require Import Lia.
5353

5454

‎logic/CornBasics.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,8 @@
4848
From Coq Require Export ZArith.
4949
From Coq Require Import Lia.
5050
Require Export CoRN.stdlib_omissions.List.
51-
Require Import Coq.Logic.Eqdep_dec.
52-
Require Import Coq.Setoids.Setoid.
51+
From Coq Require Import Eqdep_dec.
52+
From Coq Require Import Setoid.
5353

5454
Tactic Notation "apply" ":" constr(x) := pose proof x as HHH; first [
5555
refine HHH |

‎metric2/Compact.v

+3-3
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,11 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
2121
Require Import CoRN.model.totalorder.QposMinMax.
2222
Require Import CoRN.metric2.Limit.
2323
Require Export CoRN.metric2.FinEnum.
24-
Require Import Coq.ZArith.Zpow_facts.
24+
From Coq Require Import Zpow_facts.
2525
Require Export CoRN.metric2.Complete.
2626
Require Import CoRN.logic.Classic.
27-
Require Import Coq.QArith.Qpower.
28-
Require Import Coq.QArith.Qround.
27+
From Coq Require Import Qpower.
28+
From Coq Require Import Qround.
2929

3030
Set Implicit Arguments.
3131

‎metric2/Hausdorff.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ Require Import CoRN.logic.Classic.
2323
Require Export CoRN.metric2.Metric.
2424
Require Import CoRN.metric2.Classification.
2525
Require Import Coq.Lists.List.
26-
Require Import Coq.ZArith.ZArith.
26+
From Coq Require Import ZArith.
2727
Require Import CoRN.model.totalorder.QMinMax.
2828
Require Import CoRN.model.totalorder.QposMinMax.
2929

‎metric2/Limit.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
2121

2222
Require Import CoRN.algebra.RSetoid.
2323
Require Import CoRN.model.totalorder.QposMinMax.
24-
Require Import Coq.QArith.QArith.
25-
Require Import Coq.Bool.Bool.
24+
From Coq Require Import QArith.
25+
From Coq Require Import Bool.
2626
Require Export CoRN.metric2.Complete.
2727
Require Export MathClasses.theory.CoqStreams.
2828
Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals.

‎metric2/Metric.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,8 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
2020
CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
2121
*)
2222

23-
Require Export Coq.QArith.QArith.
24-
Require Import CoRN.algebra.RSetoid.
23+
From Coq Require Export QArith.
24+
Require Import CoRN.algebra.RSetoid.
2525
Require Import MathClasses.interfaces.canonical_names.
2626
Require Import MathClasses.interfaces.abstract_algebra.
2727

‎model/Zmod/ZBasics.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535
*)
3636
(* ZBasics.v, by Vince Barany *)
3737

38-
Require Export Coq.ZArith.ZArith.
38+
From Coq Require Export ZArith.
3939
Require Export CoRN.logic.CLogic.
4040
From Coq Require Import Lia.
4141

‎model/Zmod/ZDivides.v

+8-8
Original file line numberDiff line numberDiff line change
@@ -503,10 +503,10 @@ Proof.
503503
case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
504504
auto with zarith.
505505
intros p q.
506-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
506+
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
507507
intros Hlt Hp HR; rewrite HR; auto with zarith.
508508
intros p q.
509-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
509+
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
510510
case R.
511511
auto with zarith.
512512
intro r'; intros H0 H1 H2.
@@ -518,10 +518,10 @@ Proof.
518518
case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
519519
auto with zarith.
520520
intros p q.
521-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
521+
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
522522
case R; intros r' H0; intros; try (cut (Zpos r' = Zpos p); elim H0); auto with zarith.
523523
intros p q.
524-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
524+
elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
525525
case R; intros; try discriminate; try tauto.
526526
Qed.
527527

@@ -536,12 +536,12 @@ Proof.
536536
case b; unfold Z.opp in |- *.
537537
auto.
538538
intro B.
539-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
539+
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
540540
intro Hr; rewrite Hr; auto.
541541
intro B.
542542
generalize (Z_mod_lt (Zpos A) (Zpos B)).
543543
unfold Z.modulo, Z.div_eucl in |- *.
544-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
544+
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
545545
case r.
546546
intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
547547
intros R Hlt HR.
@@ -558,7 +558,7 @@ Proof.
558558
intro B.
559559
generalize (Z_mod_lt (Zpos A) (Zpos B)).
560560
unfold Z.modulo, Z.div_eucl in |- *.
561-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
561+
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
562562
case r.
563563
intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
564564
intros R Hlt HR.
@@ -572,7 +572,7 @@ Proof.
572572
intro B.
573573
generalize (Z_mod_lt (Zpos A) (Zpos B)).
574574
unfold Z.modulo, Z.div_eucl in |- *.
575-
elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
575+
elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
576576
case r.
577577
intros _ HR; fold (- q)%Z in |- *; auto.
578578
intros; discriminate.

‎model/metric2/L1metric.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,9 @@ Require Export CoRN.model.structures.StepQsec.
2626
Require Export CoRN.metric2.UniformContinuity.
2727
Require Import CoRN.metric2.Prelength.
2828
Require Import CoRN.model.structures.OpenUnit.
29-
Require Import Coq.QArith.QArith.
29+
From Coq Require Import QArith.
3030
Require Import CoRN.model.totalorder.QMinMax.
31-
Require Import Coq.QArith.Qabs.
31+
From Coq Require Import Qabs.
3232
Require Import CoRN.model.ordfields.Qordfield.
3333
Require Import CoRN.model.metric2.Qmetric.
3434
Require Import CoRN.algebra.COrdFields2.

‎model/metric2/LinfMetric.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,9 @@ Require Import CoRN.metric2.Prelength.
2727
Require Import CoRN.model.metric2.L1metric.
2828
Require Export CoRN.model.metric2.LinfMetricMonad.
2929
Require Import CoRN.model.structures.OpenUnit.
30-
Require Import Coq.QArith.QArith.
30+
From Coq Require Import QArith.
3131
Require Import CoRN.model.totalorder.QMinMax.
32-
Require Import Coq.QArith.Qabs.
32+
From Coq Require Import Qabs.
3333
Require Import CoRN.model.ordfields.Qordfield.
3434
Require Import CoRN.model.metric2.Qmetric.
3535
Require Import CoRN.algebra.COrdFields2.

‎model/metric2/LinfMetricMonad.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -29,9 +29,9 @@ Require Export CoRN.metric2.StepFunctionSetoid.
2929
Require Import CoRN.metric2.StepFunctionMonad.
3030
Require Import CoRN.metric2.UniformContinuity.
3131
Require Import CoRN.model.structures.OpenUnit.
32-
Require Import Coq.QArith.QArith.
32+
From Coq Require Import QArith.
3333
Require Import CoRN.model.totalorder.QMinMax.
34-
Require Import Coq.QArith.Qabs.
34+
From Coq Require Import Qabs.
3535
Require Import CoRN.model.ordfields.Qordfield.
3636
Require Import CoRN.model.metric2.Qmetric.
3737
Require Import CoRN.metric2.Prelength.

‎model/metric2/Qmetric.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ Require Import CoRN.metric2.Prelength.
2424
Require Import CoRN.metric2.Classification.
2525
Require Import CoRN.model.totalorder.QMinMax.
2626
Require Import CoRN.model.totalorder.QposMinMax.
27-
Require Import Coq.QArith.Qabs.
27+
From Coq Require Import Qabs.
2828
Require Import CoRN.metric2.UniformContinuity.
2929
Require Import MathClasses.implementations.stdlib_rationals.
3030

@@ -444,7 +444,7 @@ Proof with auto.
444444
apply ball_sym...
445445
Qed.
446446

447-
Require Import Coq.QArith.Qround.
447+
From Coq Require Import Qround.
448448

449449
Lemma Qfloor_ball q:
450450
Qball (1#2) ((Qfloor q # 1) + (1#2)) q.

‎model/setoids/Zfinsetoid.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@
3333
* with this work; if not, write to the Free Software Foundation, Inc.,
3434
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
3535
*)
36-
Require Export Coq.ZArith.ZArith.
36+
From Coq Require Export ZArith.
3737
Require Import CoRN.algebra.CSetoids.
3838

3939
(**

‎model/setoids/decsetoid.v

+2-5
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,8 @@
44

55
Set Implicit Arguments.
66

7-
Require Import
8-
CoRN.algebra.CSetoids
9-
Coq.Classes.SetoidDec
10-
Coq.Classes.Morphisms
11-
Coq.Classes.SetoidClass.
7+
Require Import CoRN.algebra.CSetoids.
8+
From Coq Require Import SetoidDec Morphisms SetoidClass.
129

1310

1411
Class Apartness `{SetoidClass.Setoid} (ap: Crelation A): Type :=

‎model/structures/NNUpperR.v

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
(* This module is designed to *not* be Import'ed, only Require'd. *)
22

3-
Require Import
4-
Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program.
3+
From Coq Require Import Qabs.
4+
Require Import CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec.
5+
From Coq Require Import Qminmax Ring Program.
56

67
Require CoRN.model.structures.QnonNeg.
78
Import QnonNeg.notations QnonNeg.coercions.

‎model/structures/Nsec.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,8 @@
3636

3737
(** printing {#N} $\ensuremath{\mathrel\#_{\mathbb N}}$ *)
3838

39-
Require Export Coq.Arith.Peano_dec.
40-
Require Export Coq.Relations.Relations.
39+
From Coq Require Export Peano_dec.
40+
From Coq Require Export Relations.
4141
Require Import CoRN.logic.CLogic.
4242
From Coq Require Import Lia.
4343

‎model/structures/OpenUnit.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
1818
IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
1919
CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
2020
*)
21-
Require Export Coq.QArith.QArith.
21+
From Coq Require Export QArith.
2222
Require Import CoRN.model.ordfields.Qordfield.
2323
Require Import CoRN.algebra.COrdFields.
2424
Require Import CoRN.tactics.Qauto.

‎model/structures/Qinf.v

+3-4
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
Require Import
2-
CoRN.model.totalorder.QposMinMax
3-
Coq.Setoids.Setoid Coq.Arith.Arith
4-
CoRN.model.rings.Qring CoRN.model.structures.QposInf
1+
Require Import CoRN.model.totalorder.QposMinMax.
2+
From Coq Require Import Setoid Arith.
3+
Require Import CoRN.model.rings.Qring CoRN.model.structures.QposInf
54
CoRN.stdlib_omissions.Q
65
MathClasses.interfaces.abstract_algebra
76
MathClasses.implementations.stdlib_rationals

‎model/structures/QnonNeg.v

+4-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
(* This module is designed to *not* be Import'ed, only Require'd. *)
22

3-
Require Import CoRN.model.totalorder.QposMinMax
4-
Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax.
3+
Require Import CoRN.model.totalorder.QposMinMax.
4+
From Coq Require Import Program.
5+
Require Import CoRN.model.structures.QposInf.
6+
From Coq Require Import Qminmax.
57

68

79
(* The data type and simple relations/constants: *)

‎model/structures/QposInf.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
1919
CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
2020
*)
2121

22-
Require Export Coq.QArith.QArith.
22+
From Coq Require Export QArith.
2323
Require Import CoRN.model.totalorder.QposMinMax.
2424

2525
(** printing QposInf $\mathbb{Q}^{+}_{\infty}$ #Q<SUP>+</SUP><SUB>&infin;</SUB># *)

0 commit comments

Comments
 (0)