From dbe09dd5bfc2595cb9fd96725d87d9a729cd0247 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 10 Mar 2016 13:45:37 -0500 Subject: Absolutize Coqprime imports Used ```bash cd coqprime make -kj10 cd Coqprime git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Coqprime ``` --- coqprime/Coqprime/Cyclic.v | 14 +++++++------- coqprime/Coqprime/EGroup.v | 18 +++++++++--------- coqprime/Coqprime/Euler.v | 8 ++++---- coqprime/Coqprime/FGroup.v | 8 ++++---- coqprime/Coqprime/IGroup.v | 12 ++++++------ coqprime/Coqprime/Iterator.v | 6 +++--- coqprime/Coqprime/Lagrange.v | 12 ++++++------ coqprime/Coqprime/ListAux.v | 10 +++++----- coqprime/Coqprime/LucasLehmer.v | 22 +++++++++++----------- coqprime/Coqprime/NatAux.v | 2 +- coqprime/Coqprime/PGroup.v | 18 +++++++++--------- coqprime/Coqprime/Permutation.v | 4 ++-- coqprime/Coqprime/Pmod.v | 10 +++++----- coqprime/Coqprime/Pocklington.v | 16 ++++++++-------- coqprime/Coqprime/PocklingtonCertificat.v | 16 ++++++++-------- coqprime/Coqprime/Root.v | 10 +++++----- coqprime/Coqprime/ZCAux.v | 8 ++++---- coqprime/Coqprime/ZCmisc.v | 2 +- coqprime/Coqprime/ZProgression.v | 6 +++--- coqprime/Coqprime/ZSum.v | 12 ++++++------ coqprime/Coqprime/Zp.v | 18 +++++++++--------- 21 files changed, 116 insertions(+), 116 deletions(-) (limited to 'coqprime') diff --git a/coqprime/Coqprime/Cyclic.v b/coqprime/Coqprime/Cyclic.v index c25f683ca..e2daa4d67 100644 --- a/coqprime/Coqprime/Cyclic.v +++ b/coqprime/Coqprime/Cyclic.v @@ -11,13 +11,13 @@ Proof that an abelien ring is cyclic ************************************************************************) -Require Import ZCAux. -Require Import List. -Require Import Root. -Require Import UList. -Require Import IGroup. -Require Import EGroup. -Require Import FGroup. +Require Import Coqprime.ZCAux. +Require Import Coq.Lists.List. +Require Import Coqprime.Root. +Require Import Coqprime.UList. +Require Import Coqprime.IGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/EGroup.v b/coqprime/Coqprime/EGroup.v index fd543fe04..553cb746c 100644 --- a/coqprime/Coqprime/EGroup.v +++ b/coqprime/Coqprime/EGroup.v @@ -11,15 +11,15 @@ Given an element a, create the group {e, a, a^2, ..., a^n} **********************************************************************) -Require Import ZArith. -Require Import Tactic. -Require Import List. -Require Import ZCAux. -Require Import ZArith Znumtheory. -Require Import Wf_nat. -Require Import UList. -Require Import FGroup. -Require Import Lagrange. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Lists.List. +Require Import Coqprime.ZCAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.Lagrange. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Euler.v b/coqprime/Coqprime/Euler.v index 06d92ce57..e571d8e3c 100644 --- a/coqprime/Coqprime/Euler.v +++ b/coqprime/Coqprime/Euler.v @@ -11,10 +11,10 @@ Definition of the Euler Totient function *************************************************************************) -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Export ZSum. +Require Import Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Export Coqprime.ZSum. Open Scope Z_scope. diff --git a/coqprime/Coqprime/FGroup.v b/coqprime/Coqprime/FGroup.v index a55710e7c..0bcc9ebf1 100644 --- a/coqprime/Coqprime/FGroup.v +++ b/coqprime/Coqprime/FGroup.v @@ -13,10 +13,10 @@ Definition: FGroup **********************************************************************) -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coq.ZArith.ZArith. Open Scope Z_scope. diff --git a/coqprime/Coqprime/IGroup.v b/coqprime/Coqprime/IGroup.v index 11a73d414..04219be5a 100644 --- a/coqprime/Coqprime/IGroup.v +++ b/coqprime/Coqprime/IGroup.v @@ -13,12 +13,12 @@ Definition: ZpGroup **********************************************************************) -Require Import ZArith. -Require Import Tactic. -Require Import Wf_nat. -Require Import UList. -Require Import ListAux. -Require Import FGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v index 96d3e5655..e84687cd4 100644 --- a/coqprime/Coqprime/Iterator.v +++ b/coqprime/Coqprime/Iterator.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export List. -Require Export Permutation. -Require Import Arith. +Require Export Coq.Lists.List. +Require Export Coqprime.Permutation. +Require Import Coq.Arith.Arith. Section Iterator. Variables A B : Set. diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v index b35460bad..b890c5621 100644 --- a/coqprime/Coqprime/Lagrange.v +++ b/coqprime/Coqprime/Lagrange.v @@ -14,12 +14,12 @@ Definition: lagrange **********************************************************************) -Require Import List. -Require Import UList. -Require Import ListAux. -Require Import ZArith Znumtheory. -Require Import NatAux. -Require Import FGroup. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coqprime.NatAux. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/ListAux.v b/coqprime/Coqprime/ListAux.v index c3c9602bd..4ed154685 100644 --- a/coqprime/Coqprime/ListAux.v +++ b/coqprime/Coqprime/ListAux.v @@ -11,11 +11,11 @@ Auxillary functions & Theorems **********************************************************************) -Require Export List. -Require Export Arith. -Require Export Tactic. -Require Import Inverse_Image. -Require Import Wf_nat. +Require Export Coq.Lists.List. +Require Export Coq.Arith.Arith. +Require Export Coqprime.Tactic. +Require Import Coq.Wellfounded.Inverse_Image. +Require Import Coq.Arith.Wf_nat. (************************************** Some properties on list operators: app, map,... diff --git a/coqprime/Coqprime/LucasLehmer.v b/coqprime/Coqprime/LucasLehmer.v index c3c255036..c459195a8 100644 --- a/coqprime/Coqprime/LucasLehmer.v +++ b/coqprime/Coqprime/LucasLehmer.v @@ -13,17 +13,17 @@ Definition: LucasLehmer **********************************************************************) -Require Import ZArith. -Require Import ZCAux. -Require Import Tactic. -Require Import Wf_nat. -Require Import NatAux. -Require Import UList. -Require Import ListAux. -Require Import FGroup. -Require Import EGroup. -Require Import PGroup. -Require Import IGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.ZCAux. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.NatAux. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.PGroup. +Require Import Coqprime.IGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/NatAux.v b/coqprime/Coqprime/NatAux.v index eab09150c..6df511eed 100644 --- a/coqprime/Coqprime/NatAux.v +++ b/coqprime/Coqprime/NatAux.v @@ -11,7 +11,7 @@ Auxillary functions & Theorems **********************************************************************) -Require Export Arith. +Require Export Coq.Arith.Arith. (************************************** Some properties of minus diff --git a/coqprime/Coqprime/PGroup.v b/coqprime/Coqprime/PGroup.v index e9c1b2f47..19eff5850 100644 --- a/coqprime/Coqprime/PGroup.v +++ b/coqprime/Coqprime/PGroup.v @@ -14,15 +14,15 @@ Definition: PGroup **********************************************************************) -Require Import ZArith. -Require Import Znumtheory. -Require Import Tactic. -Require Import Wf_nat. -Require Import ListAux. -Require Import UList. -Require Import FGroup. -Require Import EGroup. -Require Import IGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.ListAux. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v index a06693f89..7cb6f629d 100644 --- a/coqprime/Coqprime/Permutation.v +++ b/coqprime/Coqprime/Permutation.v @@ -11,8 +11,8 @@ Defintion and properties of permutations **********************************************************************) -Require Export List. -Require Export ListAux. +Require Export Coq.Lists.List. +Require Export Coqprime.ListAux. Section permutation. Variable A : Set. diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v index f64af48e3..45961896e 100644 --- a/coqprime/Coqprime/Pmod.v +++ b/coqprime/Coqprime/Pmod.v @@ -6,8 +6,8 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export ZArith. -Require Export ZCmisc. +Require Export Coq.ZArith.ZArith. +Require Export Coqprime.ZCmisc. Open Local Scope positive_scope. @@ -392,7 +392,7 @@ Lemma gcd_log2_mod0 : Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. -Require Import Zwf. +Require Import Coq.ZArith.Zwf. Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y). Proof. @@ -510,8 +510,8 @@ Proof. destruct (gcd_log2 b r r);intros;trivial. Qed. -Require Import ZArith. -Require Import Znumtheory. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. diff --git a/coqprime/Coqprime/Pocklington.v b/coqprime/Coqprime/Pocklington.v index 9871cd3e6..79e7dc616 100644 --- a/coqprime/Coqprime/Pocklington.v +++ b/coqprime/Coqprime/Pocklington.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Import ZCAux. -Require Import Zp. -Require Import FGroup. -Require Import EGroup. -Require Import Euler. +Require Import Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coqprime.ZCAux. +Require Import Coqprime.Zp. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.Euler. Open Scope Z_scope. diff --git a/coqprime/Coqprime/PocklingtonCertificat.v b/coqprime/Coqprime/PocklingtonCertificat.v index ed75ca281..fccea30b6 100644 --- a/coqprime/Coqprime/PocklingtonCertificat.v +++ b/coqprime/Coqprime/PocklingtonCertificat.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import List. -Require Import ZArith. -Require Import Zorder. -Require Import ZCAux. -Require Import LucasLehmer. -Require Import Pocklington. -Require Import ZCmisc. -Require Import Pmod. +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Zorder. +Require Import Coqprime.ZCAux. +Require Import Coqprime.LucasLehmer. +Require Import Coqprime.Pocklington. +Require Import Coqprime.ZCmisc. +Require Import Coqprime.Pmod. Definition dec_prime := list (positive * positive). diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v index 321865ba1..4e74a4d2f 100644 --- a/coqprime/Coqprime/Root.v +++ b/coqprime/Coqprime/Root.v @@ -11,11 +11,11 @@ Proof that a polynomial has at most n roots ************************************************************************) -Require Import ZArith. -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import Permutation. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coqprime.Permutation. Open Scope Z_scope. diff --git a/coqprime/Coqprime/ZCAux.v b/coqprime/Coqprime/ZCAux.v index de03a2fe2..aa47fb655 100644 --- a/coqprime/Coqprime/ZCAux.v +++ b/coqprime/Coqprime/ZCAux.v @@ -12,10 +12,10 @@ Auxillary functions & Theorems **********************************************************************) -Require Import ArithRing. -Require Export ZArith Zpow_facts. -Require Export Znumtheory. -Require Export Tactic. +Require Import Coq.setoid_ring.ArithRing. +Require Export Coq.ZArith.ZArith Coq.ZArith.Zpow_facts. +Require Export Coq.ZArith.Znumtheory. +Require Export Coqprime.Tactic. Theorem Zdivide_div_prime_le_square: forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x. intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith. diff --git a/coqprime/Coqprime/ZCmisc.v b/coqprime/Coqprime/ZCmisc.v index c1bdacc63..e2ec66ba1 100644 --- a/coqprime/Coqprime/ZCmisc.v +++ b/coqprime/Coqprime/ZCmisc.v @@ -6,7 +6,7 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export ZArith. +Require Export Coq.ZArith.ZArith. Open Local Scope Z_scope. Coercion Zpos : positive >-> Z. diff --git a/coqprime/Coqprime/ZProgression.v b/coqprime/Coqprime/ZProgression.v index 51ce91cdc..4cf30d692 100644 --- a/coqprime/Coqprime/ZProgression.v +++ b/coqprime/Coqprime/ZProgression.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Iterator. -Require Import ZArith. -Require Export UList. +Require Export Coqprime.Iterator. +Require Import Coq.ZArith.ZArith. +Require Export Coqprime.UList. Open Scope Z_scope. Theorem next_n_Z: forall n m, next_n Zsucc n m = n + Z_of_nat m. diff --git a/coqprime/Coqprime/ZSum.v b/coqprime/Coqprime/ZSum.v index 3a7f14065..907720f7c 100644 --- a/coqprime/Coqprime/ZSum.v +++ b/coqprime/Coqprime/ZSum.v @@ -9,12 +9,12 @@ (*********************************************************************** Summation.v from Z to Z *********************************************************************) -Require Import Arith. -Require Import ArithRing. -Require Import ListAux. -Require Import ZArith. -Require Import Iterator. -Require Import ZProgression. +Require Import Coq.Arith.Arith. +Require Import Coq.setoid_ring.ArithRing. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Iterator. +Require Import Coqprime.ZProgression. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Zp.v b/coqprime/Coqprime/Zp.v index 9b99bef1d..2f7d28d69 100644 --- a/coqprime/Coqprime/Zp.v +++ b/coqprime/Coqprime/Zp.v @@ -14,16 +14,16 @@ Definition: ZpGroup **********************************************************************) -Require Import ZArith Znumtheory Zpow_facts. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts. Require Import Coqprime.Tactic. -Require Import Wf_nat. -Require Import UList. -Require Import FGroup. -Require Import EGroup. -Require Import IGroup. -Require Import Cyclic. -Require Import Euler. -Require Import ZProgression. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. +Require Import Coqprime.Cyclic. +Require Import Coqprime.Euler. +Require Import Coqprime.ZProgression. Open Scope Z_scope. -- cgit v1.2.3