Skip to content

Commit fe8535b

Browse files
chathhorn-galoischathhorn-galois
committed
saw-core-coq: "From Coq" => "From Stdlib".
1 parent c9b9b00 commit fe8535b

File tree

11 files changed

+60
-60
lines changed

11 files changed

+60
-60
lines changed

‎saw-core-coq/coq/handwritten/CryptolToCoq/CoqVectorsExtra.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(* This file contains definitions that seemed missing from Coq.Vectors.Vector *)
22

3-
From Coq Require Import PeanoNat.
4-
From Coq.Vectors Require Vector.
3+
From Stdlib Require Import PeanoNat.
4+
From Stdlib.Vectors Require Vector.
55

66
Fixpoint zip {a b : Type} {n : nat} (xs : Vector.t a n) (ys : Vector.t b n) : Vector.t (a * b) n.
77
refine (

‎saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
(* This module contains additional definitions that can only be defined after *)
22
(* the Cryptol prelude has been defined. *)
33

4-
From Coq Require Import Lia.
5-
From Coq Require Import Lists.List.
6-
From Coq Require Import String.
7-
From Coq Require Import Vectors.Vector.
4+
From Stdlib Require Import Lia.
5+
From Stdlib Require Import Lists.List.
6+
From Stdlib Require Import String.
7+
From Stdlib Require Import Vectors.Vector.
88
From CryptolToCoq Require Import SAWCoreScaffolding.
99
From CryptolToCoq Require Import SAWCorePrelude.
1010
Import SAWCorePrelude.

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@
22
*** Lemmas about the bitvectors from SAWCoreVectorsAsCoqVectors
33
***)
44

5-
From Coq Require Import Program.Basics.
6-
From Coq Require Program.Equality.
7-
From Coq Require Import Vectors.Vector.
8-
From Coq Require Import Logic.Eqdep.
9-
From Coq Require Import Classes.RelationClasses.
10-
From Coq Require Import Classes.Morphisms.
5+
From Stdlib Require Import Program.Basics.
6+
From Stdlib Require Program.Equality.
7+
From Stdlib Require Import Vectors.Vector.
8+
From Stdlib Require Import Logic.Eqdep.
9+
From Stdlib Require Import Classes.RelationClasses.
10+
From Stdlib Require Import Classes.Morphisms.
1111

1212
From CryptolToCoq Require Import SAWCorePrelude.
1313
From CryptolToCoq Require Import SAWCoreScaffolding.

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectorsZifyU64.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
From Coq Require Import Classes.Morphisms.
2-
From Coq Require Import Lia.
3-
From Coq Require Import ZArith.BinInt.
4-
From Coq Require Import ZifyBool.
5-
From Coq Require Import ZifyClasses.
1+
From Stdlib Require Import Classes.Morphisms.
2+
From Stdlib Require Import Lia.
3+
From Stdlib Require Import ZArith.BinInt.
4+
From Stdlib Require Import ZifyBool.
5+
From Stdlib Require Import ZifyClasses.
66

77
From CryptolToCoq Require Import SAWCoreBitvectors.
88
From CryptolToCoq Require Import SAWCorePrelude.

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
From Coq Require Import Arith.Peano_dec.
2-
From Coq Require Import Arith.PeanoNat.
3-
From Coq Require Import Lists.List.
4-
From Coq Require Import Logic.Eqdep_dec.
5-
From Coq Require Import Logic.FunctionalExtensionality.
1+
From Stdlib Require Import Arith.Peano_dec.
2+
From Stdlib Require Import Arith.PeanoNat.
3+
From Stdlib Require Import Lists.List.
4+
From Stdlib Require Import Logic.Eqdep_dec.
5+
From Stdlib Require Import Logic.FunctionalExtensionality.
66
Import ListNotations.
7-
From Coq Require Import String.
8-
From Coq Require Import Vectors.Vector.
7+
From Stdlib Require Import String.
8+
From Stdlib Require Import Vectors.Vector.
99
From CryptolToCoq Require Import SAWCoreBitvectors.
1010
From CryptolToCoq Require Import SAWCoreScaffolding.
1111
From CryptolToCoq Require Import SAWCorePrelude.

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePrelude_proofs.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
From Coq Require Import Init.Nat.
2-
From Coq Require Import Lists.List.
3-
From Coq Require Import Morphisms.
4-
From Coq Require Import String.
5-
From Coq Require Import Vectors.Vector.
1+
From Stdlib Require Import Init.Nat.
2+
From Stdlib Require Import Lists.List.
3+
From Stdlib Require Import Morphisms.
4+
From Stdlib Require Import String.
5+
From Stdlib Require Import Vectors.Vector.
66

77
From CryptolToCoq Require Import SAWCorePrelude.
88
From CryptolToCoq Require Import SAWCoreScaffolding.

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
From Coq Require Import ZArith.BinInt.
2-
From Coq Require Import ZArith.Zdiv.
3-
From Coq Require Import NArith.NArith.
4-
From Coq Require Import Lists.List.
5-
From Coq Require Numbers.NatInt.NZLog.
6-
From Coq Require Import Strings.String.
7-
From Coq Require Export Logic.Eqdep.
8-
From Coq Require Import Arith.PeanoNat.
1+
From Stdlib Require Import ZArith.BinInt.
2+
From Stdlib Require Import ZArith.Zdiv.
3+
From Stdlib Require Import NArith.NArith.
4+
From Stdlib Require Import Lists.List.
5+
From Stdlib Require Numbers.NatInt.NZLog.
6+
From Stdlib Require Import Strings.String.
7+
From Stdlib Require Export Logic.Eqdep.
8+
From Stdlib Require Import Arith.PeanoNat.
99

1010

1111
(***

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffoldingCopy.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
From Coq Require Import Lists.List.
2-
From Coq Require Import Numbers.NatInt.NZLog.
3-
From Coq Require Import Strings.String.
1+
From Stdlib Require Import Lists.List.
2+
From Stdlib Require Import Numbers.NatInt.NZLog.
3+
From Stdlib Require Import Strings.String.
44

55
From Ornamental Require Import Ornaments.
66

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqLists.v‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
From Coq.Lists Require Import List.
2-
From Coq.Numbers.NatInt Require NZLog.
3-
From Coq.Strings Require String.
4-
From CryptolToCoq Require Import SAWCoreScaffolding.
5-
From Coq Require Import ZifyClasses.
1+
From Stdlib.Lists Require Import List.
2+
From Stdlib.Numbers.NatInt Require NZLog.
3+
From Stdlib.Strings Require String.
4+
From CryptolToCoq Require Import SAWCoreScaffolding.
5+
From Stdlib Require Import ZifyClasses.
66

77
Import ListNotations.
88

‎saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
From Bits Require Import operations.
22
From Bits Require Import spec.
33

4-
From Coq Require Import FunctionalExtensionality.
5-
From Coq Require Import Lists.List.
6-
From Coq Require Numbers.NatInt.NZLog.
7-
From Coq Require Import Peano_dec.
8-
From Coq Require Import PeanoNat.
9-
From Coq Require Import Strings.String.
10-
From Coq Require Import Vectors.Vector.
11-
From Coq Require Import Bool.Bool.
12-
From Coq Require Import BinNums.
13-
From Coq Require Import ZifyClasses.
4+
From Stdlib Require Import FunctionalExtensionality.
5+
From Stdlib Require Import Lists.List.
6+
From Stdlib Require Numbers.NatInt.NZLog.
7+
From Stdlib Require Import Peano_dec.
8+
From Stdlib Require Import PeanoNat.
9+
From Stdlib Require Import Strings.String.
10+
From Stdlib Require Import Vectors.Vector.
11+
From Stdlib Require Import Bool.Bool.
12+
From Stdlib Require Import BinNums.
13+
From Stdlib Require Import ZifyClasses.
1414

1515
From CryptolToCoq Require Import SAWCoreScaffolding.
1616

@@ -20,8 +20,8 @@ From mathcomp Require Import ssrbool.
2020
From mathcomp Require Import fintype.
2121
From mathcomp Require Import tuple.
2222

23-
From Coq Require Export ZArith.BinIntDef.
24-
From Coq Require Export PArith.BinPos.
23+
From Stdlib Require Export ZArith.BinIntDef.
24+
From Stdlib Require Export PArith.BinPos.
2525

2626
Import VectorNotations.
2727

0 commit comments

Comments
 (0)