diff options
author | 2017-03-30 16:53:15 -0400 | |
---|---|---|
committer | 2017-03-30 16:58:50 -0400 | |
commit | 8497deb05c2707a5b17286bc6ed1eb8e0ee28a69 (patch) | |
tree | 30069168f605ab3b914d65870f528347516e5527 /src | |
parent | cb9e18103c6fe0580fa6598380b6c6ec66d261a0 (diff) |
change import order to avoid name-clash with [List.repeat] and [Tuple.repeat]
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/GF1305.v | 2 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 717417209..6ddc12ee5 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -5,10 +5,10 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.Util.Tuple. Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Tuple. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 0cea13d43..5c5c5741d 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -5,10 +5,10 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.Util.Tuple. Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tower. |