From 3eab786d92b348c1dec33640eec3a02a5a86606b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Sep 2016 11:22:45 -0700 Subject: Fully qualify [Require]s This way they won't become ambiguous if we add new files --- src/Assembly/AlmostConversion.v | 4 ++-- src/Assembly/AlmostQhasm.v | 6 ++--- src/Assembly/Conversion.v | 2 +- src/Assembly/PseudoConversion.v | 20 ++++++++--------- src/Assembly/Qhasm.v | 7 +++--- src/Assembly/QhasmCommon.v | 8 +++---- src/Assembly/StringConversion.v | 26 +++++++++++----------- .../ModularBaseSystemListProofs.v | 16 ++++++------- src/ModularArithmetic/Pow2Base.v | 2 +- .../PseudoMersenneBaseParamProofs.v | 6 ++--- src/ModularArithmetic/PseudoMersenneBaseParams.v | 4 ++-- src/Spec/EdDSA.v | 6 ++--- src/Tactics/Algebra_syntax/Nsatz.v | 2 +- src/Util/AdditionChainExponentiation.v | 6 ++--- src/Util/Sum.v | 2 +- src/Util/Tuple.v | 6 ++--- src/Util/Unit.v | 2 +- 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). -- cgit v1.2.3