Fully qualify [Require]s

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

4 files changed, 8 insertions, 8 deletions

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).