Skip to content

Commit c7ed589

Browse files
proux01JasonGross
authored andcommitted
1 parent 781d047 commit c7ed589

File tree

2 files changed

+6
-2
lines changed

2 files changed

+6
-2
lines changed

src/Bedrock/End2End/RupicolaCrypto/Broadcast.v

+3-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,9 @@ From Coq Require Import Utf8.
22
Require Import Rupicola.Lib.Api.
33
Require Import Rupicola.Lib.Loops.
44

5-
From Coq Require Init.Byte String. Import Init.Byte(byte(..)) String.
5+
From Coq Require Init.Byte String.
6+
From Coq Require Import Init.Byte(byte(..)).
7+
Import String.
68
Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
79
From Coq Require Import BinInt. Import Zdiv. Local Open Scope Z_scope.
810
Require Import coqutil.Byte coqutil.Word.LittleEndianList.

src/Bedrock/End2End/RupicolaCrypto/Spec.v

+3-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
From Coq Require Init.Byte String. Export Init.Byte(byte(..)) String.
1+
From Coq Require Init.Byte String.
2+
From Coq Require Export Init.Byte(byte(..)).
3+
Export String.
24
Require Export coqutil.Datatypes.List. Export Lists.List List.ListNotations.
35
From Coq Require Export BinInt. Export Zdiv. Local Open Scope Z_scope.
46
Require Export coqutil.Byte coqutil.Word.LittleEndianList.

0 commit comments

Comments
 (0)