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
```

21 files changed, 116 insertions, 116 deletions

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.