Fully qualify [Require]s

This way they won't become ambiguous if we add new files

17 files changed, 62 insertions, 63 deletions

diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v
index 878aa37bf..3e42ae6d5 100644
--- a/src/Assembly/AlmostConversion.v
+++ b/src/Assembly/AlmostConversion.v
@@ -1,6 +1,6 @@
 
-Require Import NArith.
-Require Export Qhasm AlmostQhasm Conversion.
+Require Import Coq.NArith.NArith.
+Require Export Crypto.Assembly.Qhasm Crypto.Assembly.AlmostQhasm Crypto.Assembly.Conversion.
 
 Module AlmostConversion <: Conversion AlmostQhasm Qhasm.
   Import QhasmCommon AlmostQhasm Qhasm.
diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
index f3ed925c7..e91e20843 100644
--- a/src/Assembly/AlmostQhasm.v
+++ b/src/Assembly/AlmostQhasm.v
@@ -1,6 +1,6 @@
-Require Import QhasmCommon QhasmEvalCommon.
-Require Import Language.
-Require Import List.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon.
+Require Import Crypto.Assembly.Language.
+Require Import Coq.Lists.List.
 
 Module AlmostQhasm <: Language.
   Import QhasmEval.
diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v
index 239bd6b71..cf0eba23a 100644
--- a/src/Assembly/Conversion.v
+++ b/src/Assembly/Conversion.v
@@ -1,5 +1,5 @@
 
-Require Export Language.
+Require Export Crypto.Assembly.Language.
 
 Module Type Conversion (A B: Language).
 
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 9959e5319..d5fb098b0 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -1,7 +1,7 @@
-Require Export Language Conversion QhasmCommon QhasmEvalCommon QhasmUtil.
-Require Export Pseudo AlmostQhasm State.
-Require Import Bedrock.Word NArith NPeano Euclid.
-Require Import List Sumbool Vector.
+Require Export Crypto.Assembly.Language Crypto.Assembly.Conversion Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil.
+Require Export Crypto.Assembly.Pseudo Crypto.Assembly.AlmostQhasm Crypto.Assembly.State.
+Require Import Bedrock.Word Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Euclid.
+Require Import Coq.Lists.List Coq.Bool.Sumbool Coq.Vectors.Vector.
 
 Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
   Import AlmostQhasm EvalUtil ListState Pseudo ListNotations.
@@ -83,7 +83,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
         Some (ASkip, [get i sM M], madd i sM M, F)
 
       | PVar n None i => (* assign to register by default *)
-        Some (ASkip, [get i rM M], madd i rM M, F) 
+        Some (ASkip, [get i rM M], madd i rM M, F)
 
       | PConst n c =>
         Some (AAssign (AConstInt (reg' start) (const' c)),
@@ -157,7 +157,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
           end
         end
 
-      | PComb n a b f g => 
+      | PComb n a b f g =>
         match (convertProgram' f start M F) with
         | None => None
         | Some (fp, fm, M', F') =>
@@ -167,7 +167,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
             end
         end
 
-      | PIf n m o i0 i1 l r => 
+      | PIf n m o i0 i1 l r =>
         match (convertProgram' l start M F) with
         | None => None
         | Some (lp, lr, lM, lF) =>
@@ -187,9 +187,9 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
             end
         end
 
-      | PFunExp n f e => 
+      | PFunExp n f e =>
         match (convertProgram' f (S start) M F) with
-        | Some (fp, fr, M', F') => 
+        | Some (fp, fr, M', F') =>
             let a := start in
             Some (ASeq
             (AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
@@ -211,7 +211,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
 
   End Conv.
 
-  Definition convertProgram x y (prog: Program x) : option (AlmostQhasm.Program y) := 
+  Definition convertProgram x y (prog: Program x) : option (AlmostQhasm.Program y) :=
     let vs := max (inputs x) (outputs x) in
     let M0 := mempty (width x) in
     let F0 := fempty (width x) in
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
index 9ba2c0a56..0d4e06a85 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -1,6 +1,6 @@
-Require Import QhasmCommon QhasmEvalCommon.
-Require Import Language.
-Require Import List NPeano.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon.
+Require Import Crypto.Assembly.Language.
+Require Import Coq.Lists.List Coq.Numbers.Natural.Peano.NPeano.
 
 Module Qhasm <: Language.
   Import ListNotations.
@@ -84,4 +84,3 @@ Module Qhasm <: Language.
 
   (* world peace *)
 End Qhasm.
-
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 908d16037..40619ff08 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -1,4 +1,4 @@
-Require Export String List NPeano NArith.
+Require Export Coq.Strings.String Coq.Lists.List Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
 Require Export Bedrock.Word.
 
 (* Utilities *)
@@ -85,9 +85,9 @@ Inductive TestOp :=
   | TGt: TestOp   | TGe: TestOp.
 
 Inductive Conditional :=
-  | CTrue: Conditional 
-  | CZero: forall n, Reg n -> Conditional 
-  | CReg: forall n, TestOp -> Reg n -> Reg n -> Conditional 
+  | CTrue: Conditional
+  | CZero: forall n, Reg n -> Conditional
+  | CReg: forall n, TestOp -> Reg n -> Reg n -> Conditional
   | CConst: forall n, TestOp -> Reg n -> Const n -> Conditional.
 
 (* Generalized Variable Entry *)
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 9f3908a26..5113b0062 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -1,7 +1,7 @@
-Require Export Language Conversion.
-Require Export String Ascii Basics Sumbool.
-Require Import QhasmCommon QhasmEvalCommon QhasmUtil Qhasm.
-Require Import NArith NPeano.
+Require Export Crypto.Assembly.Language Crypto.Assembly.Conversion.
+Require Export Coq.Strings.String Coq.Strings.Ascii Coq.Program.Basics Coq.Bool.Sumbool.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Qhasm.
+Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano.
 Require Export Bedrock.Word.
 
 Module QhasmString <: Language.
@@ -55,10 +55,10 @@ Module StringConversion <: Conversion Qhasm QhasmString.
   Section Elements.
     Local Open Scope string_scope.
 
-    Definition nameSuffix (n: nat): string := 
+    Definition nameSuffix (n: nat): string :=
       (nToHex (N.of_nat n)).
 
-    Coercion wordToString {n} (w: word n): string := 
+    Coercion wordToString {n} (w: word n): string :=
       "0x" ++ (nToHex (wordToN w)).
 
     Coercion constToString {n} (c: Const n): string :=
@@ -119,13 +119,13 @@ Module StringConversion <: Conversion Qhasm QhasmString.
       match b with
       | AddWithCarry => "+"
       end.
- 
+
     Coercion rotOpToString (r: RotOp): string :=
       match r with
       | Shl => "<<"
       | Shr => ">>"
       end.
- 
+
     Definition operationToString (op: Operation): option string :=
       let f := fun x => (
         if (Nat.eq_dec x 32)
@@ -135,7 +135,7 @@ Module StringConversion <: Conversion Qhasm QhasmString.
           else "128") in
 
       match op with
-      | IOpConst n o r c => 
+      | IOpConst n o r c =>
         r ++ " " ++ o ++ "= " ++ c
       | IOpReg n o a b =>
         a ++ " " ++ o ++ "= " ++ b
@@ -166,9 +166,9 @@ Module StringConversion <: Conversion Qhasm QhasmString.
 
     Definition conditionalToString (c: Conditional): string * string :=
       match c with
-      | CTrue => ("=? 0", "=") 
+      | CTrue => ("=? 0", "=")
       | CZero n r => ("=? " ++ r, "=")
-      | CReg n t a b => 
+      | CReg n t a b =>
         match (testOpToString t) with
         | (true, s) =>
           (s ++ "? " ++ a ++ " - " ++ b, s)
@@ -176,9 +176,9 @@ Module StringConversion <: Conversion Qhasm QhasmString.
           (s ++ "? " ++ a ++ " - " ++ b, "!" ++ s)
         end
 
-      | CConst n t a b => 
+      | CConst n t a b =>
         match (testOpToString t) with
-        | (true, s) => 
+        | (true, s) =>
           (s ++ "? " ++ a ++ " - " ++ b, s)
         | (false, s) =>
           (s ++ "? " ++ a ++ " - " ++ b, "!" ++ s)
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
index 16699b8a2..48c4f2402 100644
--- a/src/ModularArithmetic/ModularBaseSystemListProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -1,7 +1,7 @@
-Require Import Zpower ZArith.
+Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import List.
-Require Import VerdiTactics.
+Require Import Coq.Lists.List.
+Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.BaseSystemProofs.
 Require Import Crypto.ModularArithmetic.Pow2Base.
 Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
@@ -58,8 +58,8 @@ Section LengthProofs.
                | |- 2 ^ _ <> 0 => apply Z.pow_nonzero
                | |- _ => solve [apply BaseSystem.b0_1]
                | |- _ => solve [auto using limb_widths_nonneg, sum_firstn_limb_widths_nonneg, limb_widths_match_modulus]
-               | |- _ => omega 
-               | |- _ => congruence 
+               | |- _ => omega
+               | |- _ => congruence
                end.
   Qed.
 
@@ -117,7 +117,7 @@ Section LengthProofs.
     apply Min.min_case; omega.
   Qed.
   Hint Rewrite @length_conditional_subtract_modulus : distr_length.
-  
+
   Lemma length_freeze {u} :
     length u = length limb_widths
     -> length (freeze u) = length limb_widths.
@@ -133,7 +133,7 @@ Section LengthProofs.
     cbv [pack]; intros.
     apply Pow2BaseProofs.length_convert.
   Qed.
-  
+
   Lemma length_unpack : forall {target_widths}
                              {target_widths_nonneg : forall x, In x target_widths -> 0 <= x}
                              {pf us},
@@ -143,4 +143,4 @@ Section LengthProofs.
     apply Pow2BaseProofs.length_convert.
   Qed.
 
-End LengthProofs.
\ No newline at end of file
+End LengthProofs.
diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
index bb2f34ad4..0175018f8 100644
--- a/src/ModularArithmetic/Pow2Base.v
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -1,4 +1,4 @@
-Require Import Zpower ZArith.
+Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ZUtil.
 Require Crypto.BaseSystem.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 4b3af84e1..630fc102e 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -1,9 +1,9 @@
-Require Import Zpower ZArith.
-Require Import List.
+Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import VerdiTactics.
+Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.BaseSystem.
 Require Import Crypto.BaseSystemProofs.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v
index 1f9a0f2f6..b564bcb05 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParams.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v
@@ -1,5 +1,5 @@
-Require Import ZArith.
-Require Import List.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
 Require Import Crypto.Util.ListUtil.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 25109bc4c..38dc64cef 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -13,7 +13,7 @@ Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
 Module Import Notations.
   Import NPeano Nat.
-  
+
   Infix "^" := pow.
   Infix "mod" := modulo (at level 40, no associativity).
   Infix "++" := Word.combine.
@@ -64,7 +64,7 @@ Section EdDSA.
   Local Arguments H {n} _.
   Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing).
 
-  Require Import Omega.
+  Require Import Coq.omega.Omega.
   Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega.
 
   Program Definition curveKey (sk:secretkey) : nat :=
@@ -90,4 +90,4 @@ Section EdDSA.
     ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat),
       S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A
       -> valid message (Eenc A) (Eenc R ++ Senc S).
-End EdDSA.
\ No newline at end of file
+End EdDSA.
diff --git a/src/Tactics/Algebra_syntax/Nsatz.v b/src/Tactics/Algebra_syntax/Nsatz.v
index a5b04cfa2..b59f68120 100644
--- a/src/Tactics/Algebra_syntax/Nsatz.v
+++ b/src/Tactics/Algebra_syntax/Nsatz.v
@@ -1,6 +1,6 @@
 (*** Tactics for manipulating polynomial equations *)
 Require Coq.nsatz.Nsatz.
-Require Import List.
+Require Import Coq.Lists.List.
 
 Generalizable All Variables.
 Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
index b0aae0f91..cf8a68340 100644
--- a/src/Util/AdditionChainExponentiation.v
+++ b/src/Util/AdditionChainExponentiation.v
@@ -1,8 +1,8 @@
 Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations.
 Require Import Coq.Numbers.BinNums Coq.NArith.BinNat.
 Require Import Crypto.Util.ListUtil.
-Require Import Algebra. Import Monoid ScalarMult.
-Require Import VerdiTactics.
+Require Import Crypto.Algebra. Import Monoid ScalarMult.
+Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.Option.
 
 Section AddChainExp.
@@ -56,4 +56,4 @@ Section AddChainExp.
     destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil;
       rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity.
   Qed.
-End AddChainExp.
\ No newline at end of file
+End AddChainExp.
diff --git a/src/Util/Sum.v b/src/Util/Sum.v
index 1ee8ea69a..51d52b12d 100644
--- a/src/Util/Sum.v
+++ b/src/Util/Sum.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Util.Decidable.
 
 Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B)
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 568c3ce21..76064e7b4 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 
@@ -162,7 +162,7 @@ Arguments fieldwiseb {A B n} _ _ _.
 
 Lemma fieldwiseb'_fieldwise' :forall {A B} n R Rb
                                    (a:tuple' A n) (b:tuple' B n),
-  (forall a b, Rb a b = true <-> R a b) -> 
+  (forall a b, Rb a b = true <-> R a b) ->
   (fieldwiseb' Rb a b = true <-> fieldwise' R a b).
 Proof.
   intros.
@@ -176,7 +176,7 @@ Qed.
 
 Lemma fieldwiseb_fieldwise :forall {A B} n R Rb
                                    (a:tuple A n) (b:tuple B n),
-  (forall a b, Rb a b = true <-> R a b) -> 
+  (forall a b, Rb a b = true <-> R a b) ->
   (fieldwiseb Rb a b = true <-> fieldwise R a b).
 Proof.
   intros; destruct n; simpl @tuple in *;
diff --git a/src/Util/Unit.v b/src/Util/Unit.v
index cf5c4f669..637c3daeb 100644
--- a/src/Util/Unit.v
+++ b/src/Util/Unit.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
 
 (* an equivalence for a relation on trivial things, like [unit] *)
 Global Instance Equivalence_trivial {A} : Equivalence (fun _ _ : A => True).