Skip to content

Commit cc4cf46

Browse files
chathhorn-galoischathhorn-galois
committed
saw-core-coq: remove duplicate imports.
1 parent 29b304d commit cc4cf46

12 files changed

+0
-187
lines changed

‎otherTests/saw-core-coq/test_arithmetic.log.good‎

Lines changed: 0 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -39,9 +37,7 @@ Import VectorNotations.
3937

4038
(** Post-preamble section specified by you *)
4139
From CryptolToCoq Require Import SAWCorePrelude.
42-
Import SAWCorePrelude.
4340
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
44-
Import CryptolPrimitivesForSAWCore.
4541

4642

4743
(** Code generated by saw-core-coq *)
@@ -66,9 +62,7 @@ Import VectorNotations.
6662

6763
(** Post-preamble section specified by you *)
6864
From CryptolToCoq Require Import SAWCorePrelude.
69-
Import SAWCorePrelude.
7065
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
71-
Import CryptolPrimitivesForSAWCore.
7266

7367

7468
(** Code generated by saw-core-coq *)
@@ -93,9 +87,7 @@ Import VectorNotations.
9387

9488
(** Post-preamble section specified by you *)
9589
From CryptolToCoq Require Import SAWCorePrelude.
96-
Import SAWCorePrelude.
9790
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
98-
Import CryptolPrimitivesForSAWCore.
9991

10092

10193
(** Code generated by saw-core-coq *)
@@ -120,9 +112,7 @@ Import VectorNotations.
120112

121113
(** Post-preamble section specified by you *)
122114
From CryptolToCoq Require Import SAWCorePrelude.
123-
Import SAWCorePrelude.
124115
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
125-
Import CryptolPrimitivesForSAWCore.
126116

127117

128118
(** Code generated by saw-core-coq *)
@@ -148,9 +138,7 @@ Import VectorNotations.
148138

149139
(** Post-preamble section specified by you *)
150140
From CryptolToCoq Require Import SAWCorePrelude.
151-
Import SAWCorePrelude.
152141
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
153-
Import CryptolPrimitivesForSAWCore.
154142

155143

156144
(** Code generated by saw-core-coq *)
@@ -175,9 +163,7 @@ Import VectorNotations.
175163

176164
(** Post-preamble section specified by you *)
177165
From CryptolToCoq Require Import SAWCorePrelude.
178-
Import SAWCorePrelude.
179166
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
180-
Import CryptolPrimitivesForSAWCore.
181167

182168

183169
(** Code generated by saw-core-coq *)
@@ -201,9 +187,7 @@ Import VectorNotations.
201187

202188
(** Post-preamble section specified by you *)
203189
From CryptolToCoq Require Import SAWCorePrelude.
204-
Import SAWCorePrelude.
205190
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
206-
Import CryptolPrimitivesForSAWCore.
207191

208192

209193
(** Code generated by saw-core-coq *)
@@ -227,9 +211,7 @@ Import VectorNotations.
227211

228212
(** Post-preamble section specified by you *)
229213
From CryptolToCoq Require Import SAWCorePrelude.
230-
Import SAWCorePrelude.
231214
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
232-
Import CryptolPrimitivesForSAWCore.
233215

234216

235217
(** Code generated by saw-core-coq *)
@@ -252,9 +234,7 @@ Import VectorNotations.
252234

253235
(** Post-preamble section specified by you *)
254236
From CryptolToCoq Require Import SAWCorePrelude.
255-
Import SAWCorePrelude.
256237
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
257-
Import CryptolPrimitivesForSAWCore.
258238

259239

260240
(** Code generated by saw-core-coq *)
@@ -277,9 +257,7 @@ Import VectorNotations.
277257

278258
(** Post-preamble section specified by you *)
279259
From CryptolToCoq Require Import SAWCorePrelude.
280-
Import SAWCorePrelude.
281260
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
282-
Import CryptolPrimitivesForSAWCore.
283261

284262

285263
(** Code generated by saw-core-coq *)
@@ -317,9 +295,7 @@ Import VectorNotations.
317295

318296
(** Post-preamble section specified by you *)
319297
From CryptolToCoq Require Import SAWCorePrelude.
320-
Import SAWCorePrelude.
321298
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
322-
Import CryptolPrimitivesForSAWCore.
323299

324300

325301
(** Code generated by saw-core-coq *)

‎otherTests/saw-core-coq/test_boolean.log.good‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -34,9 +32,7 @@ Import VectorNotations.
3432

3533
(** Post-preamble section specified by you *)
3634
From CryptolToCoq Require Import SAWCorePrelude.
37-
Import SAWCorePrelude.
3835
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
39-
Import CryptolPrimitivesForSAWCore.
4036

4137

4238
(** Code generated by saw-core-coq *)
@@ -59,9 +55,7 @@ Import VectorNotations.
5955

6056
(** Post-preamble section specified by you *)
6157
From CryptolToCoq Require Import SAWCorePrelude.
62-
Import SAWCorePrelude.
6358
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
64-
Import CryptolPrimitivesForSAWCore.
6559

6660

6761
(** Code generated by saw-core-coq *)
@@ -90,9 +84,7 @@ Import VectorNotations.
9084

9185
(** Post-preamble section specified by you *)
9286
From CryptolToCoq Require Import SAWCorePrelude.
93-
Import SAWCorePrelude.
9487
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
95-
Import CryptolPrimitivesForSAWCore.
9688

9789

9890
(** Code generated by saw-core-coq *)
@@ -117,9 +109,7 @@ Import VectorNotations.
117109

118110
(** Post-preamble section specified by you *)
119111
From CryptolToCoq Require Import SAWCorePrelude.
120-
Import SAWCorePrelude.
121112
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
122-
Import CryptolPrimitivesForSAWCore.
123113

124114

125115
(** Code generated by saw-core-coq *)

‎otherTests/saw-core-coq/test_cryptol_module_simple.log.good‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,8 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import SAWCorePreludeExtra.
1514
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
16-
Import CryptolPrimitivesForSAWCore.
1715
From CryptolToCoq Require Import CryptolPrimitivesForSAWCoreExtra.
1816

1917

‎otherTests/saw-core-coq/test_cryptol_primitives.log.good‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import SAWCorePreludeExtra.
1514

1615

‎otherTests/saw-core-coq/test_lambda.log.good‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -38,9 +36,7 @@ Import VectorNotations.
3836

3937
(** Post-preamble section specified by you *)
4038
From CryptolToCoq Require Import SAWCorePrelude.
41-
Import SAWCorePrelude.
4239
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
43-
Import CryptolPrimitivesForSAWCore.
4440

4541

4642
(** Code generated by saw-core-coq *)
@@ -66,9 +62,7 @@ Import VectorNotations.
6662

6763
(** Post-preamble section specified by you *)
6864
From CryptolToCoq Require Import SAWCorePrelude.
69-
Import SAWCorePrelude.
7065
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
71-
Import CryptolPrimitivesForSAWCore.
7266

7367

7468
(** Code generated by saw-core-coq *)
@@ -93,9 +87,7 @@ Import VectorNotations.
9387

9488
(** Post-preamble section specified by you *)
9589
From CryptolToCoq Require Import SAWCorePrelude.
96-
Import SAWCorePrelude.
9790
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
98-
Import CryptolPrimitivesForSAWCore.
9991

10092

10193
(** Code generated by saw-core-coq *)
@@ -123,9 +115,7 @@ Import VectorNotations.
123115

124116
(** Post-preamble section specified by you *)
125117
From CryptolToCoq Require Import SAWCorePrelude.
126-
Import SAWCorePrelude.
127118
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
128-
Import CryptolPrimitivesForSAWCore.
129119

130120

131121
(** Code generated by saw-core-coq *)

‎otherTests/saw-core-coq/test_literals.log.good‎

Lines changed: 0 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -34,9 +32,7 @@ Import VectorNotations.
3432

3533
(** Post-preamble section specified by you *)
3634
From CryptolToCoq Require Import SAWCorePrelude.
37-
Import SAWCorePrelude.
3835
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
39-
Import CryptolPrimitivesForSAWCore.
4036

4137

4238
(** Code generated by saw-core-coq *)
@@ -67,9 +63,7 @@ Import VectorNotations.
6763

6864
(** Post-preamble section specified by you *)
6965
From CryptolToCoq Require Import SAWCorePrelude.
70-
Import SAWCorePrelude.
7166
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
72-
Import CryptolPrimitivesForSAWCore.
7367

7468

7569
(** Code generated by saw-core-coq *)
@@ -106,9 +100,7 @@ Import VectorNotations.
106100

107101
(** Post-preamble section specified by you *)
108102
From CryptolToCoq Require Import SAWCorePrelude.
109-
Import SAWCorePrelude.
110103
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
111-
Import CryptolPrimitivesForSAWCore.
112104

113105

114106
(** Code generated by saw-core-coq *)
@@ -142,9 +134,7 @@ Import VectorNotations.
142134

143135
(** Post-preamble section specified by you *)
144136
From CryptolToCoq Require Import SAWCorePrelude.
145-
Import SAWCorePrelude.
146137
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
147-
Import CryptolPrimitivesForSAWCore.
148138

149139

150140
(** Code generated by saw-core-coq *)
@@ -173,9 +163,7 @@ Import VectorNotations.
173163

174164
(** Post-preamble section specified by you *)
175165
From CryptolToCoq Require Import SAWCorePrelude.
176-
Import SAWCorePrelude.
177166
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
178-
Import CryptolPrimitivesForSAWCore.
179167

180168

181169
(** Code generated by saw-core-coq *)
@@ -200,9 +188,7 @@ Import VectorNotations.
200188

201189
(** Post-preamble section specified by you *)
202190
From CryptolToCoq Require Import SAWCorePrelude.
203-
Import SAWCorePrelude.
204191
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
205-
Import CryptolPrimitivesForSAWCore.
206192

207193

208194
(** Code generated by saw-core-coq *)
@@ -225,9 +211,7 @@ Import VectorNotations.
225211

226212
(** Post-preamble section specified by you *)
227213
From CryptolToCoq Require Import SAWCorePrelude.
228-
Import SAWCorePrelude.
229214
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
230-
Import CryptolPrimitivesForSAWCore.
231215

232216

233217
(** Code generated by saw-core-coq *)
@@ -249,9 +233,7 @@ Import VectorNotations.
249233

250234
(** Post-preamble section specified by you *)
251235
From CryptolToCoq Require Import SAWCorePrelude.
252-
Import SAWCorePrelude.
253236
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
254-
Import CryptolPrimitivesForSAWCore.
255237

256238

257239
(** Code generated by saw-core-coq *)
@@ -274,9 +256,7 @@ Import VectorNotations.
274256

275257
(** Post-preamble section specified by you *)
276258
From CryptolToCoq Require Import SAWCorePrelude.
277-
Import SAWCorePrelude.
278259
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
279-
Import CryptolPrimitivesForSAWCore.
280260

281261

282262
(** Code generated by saw-core-coq *)
@@ -299,9 +279,7 @@ Import VectorNotations.
299279

300280
(** Post-preamble section specified by you *)
301281
From CryptolToCoq Require Import SAWCorePrelude.
302-
Import SAWCorePrelude.
303282
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
304-
Import CryptolPrimitivesForSAWCore.
305283

306284

307285
(** Code generated by saw-core-coq *)
@@ -324,9 +302,7 @@ Import VectorNotations.
324302

325303
(** Post-preamble section specified by you *)
326304
From CryptolToCoq Require Import SAWCorePrelude.
327-
Import SAWCorePrelude.
328305
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
329-
Import CryptolPrimitivesForSAWCore.
330306

331307

332308
(** Code generated by saw-core-coq *)
@@ -349,9 +325,7 @@ Import VectorNotations.
349325

350326
(** Post-preamble section specified by you *)
351327
From CryptolToCoq Require Import SAWCorePrelude.
352-
Import SAWCorePrelude.
353328
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
354-
Import CryptolPrimitivesForSAWCore.
355329

356330

357331
(** Code generated by saw-core-coq *)
@@ -373,9 +347,7 @@ Import VectorNotations.
373347

374348
(** Post-preamble section specified by you *)
375349
From CryptolToCoq Require Import SAWCorePrelude.
376-
Import SAWCorePrelude.
377350
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
378-
Import CryptolPrimitivesForSAWCore.
379351

380352

381353
(** Code generated by saw-core-coq *)

0 commit comments

Comments
 (0)