Skip to content

Commit 6ca018c

Browse files
mpetruskampetruska
committed
Rename PlutusV3 directory to Uplc (resolves #1)
1 parent c24f20d commit 6ca018c

File tree

17 files changed

+48
-43
lines changed

17 files changed

+48
-43
lines changed

‎theories/Cbor/Encoding.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ From CoqUplc Require Import Prelude.Bytes.
1010
From CoqUplc Require Import Prelude.FunctionalNotations.
1111
From CoqUplc Require Import Prelude.Option.
1212

13-
From CoqUplc Require Import PlutusV3.Uplc.
13+
From CoqUplc Require Import Uplc.Term.
1414

1515
Local Open Scope bool_scope.
1616
Local Open Scope N_scope.

‎theories/Examples/Examples01.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ From Coq Require Import Lists.List.
33
From Coq Require Import Strings.String.
44
From Coq Require Import ZArith.
55

6-
From CoqUplc Require Import PlutusV3.Builtins.
6+
From CoqUplc Require Import Uplc.Builtins.
77
Import ExpectedArgNotations.
8-
From CoqUplc Require Import PlutusV3.CekMachine.
9-
From CoqUplc Require Import PlutusV3.CekValue.
10-
From CoqUplc Require Import PlutusV3.Uplc.
8+
From CoqUplc Require Import Uplc.CekMachine.
9+
From CoqUplc Require Import Uplc.CekValue.
10+
From CoqUplc Require Import Uplc.Term.
1111

1212
Local Open Scope expectedArgs_scope.
1313

‎theories/Examples/Examples02.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@ From Coq Require Import ZArith.
88
From CoqUplc Require Import Unicode.String.
99
From CoqUplc Require Import Unicode.StringShow.
1010

11-
From CoqUplc Require Import PlutusV3.CekMachine.
12-
From CoqUplc Require Import PlutusV3.CekValue.
13-
From CoqUplc Require Import PlutusV3.Uplc.
11+
From CoqUplc Require Import Uplc.CekMachine.
12+
From CoqUplc Require Import Uplc.CekValue.
13+
From CoqUplc Require Import Uplc.Term.
1414

1515
Local Open Scope string_scope.
1616
Local Open Scope Z_scope.

theories/PlutusV3/BuiltinFunctions/Bool.v renamed to theories/Uplc/BuiltinFunctions/Bool.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
From Coq Require Import Lists.List.
22
Import ListNotations.
33

4-
From CoqUplc Require Import PlutusV3.CekValue.
5-
From CoqUplc Require Import PlutusV3.Uplc.
4+
From CoqUplc Require Import Uplc.CekValue.
5+
From CoqUplc Require Import Uplc.Term.
66

77
Definition ifThenElse (Vs : list cekValue) : option cekValue :=
88
match Vs with

theories/PlutusV3/BuiltinFunctions/ByteString.v renamed to theories/Uplc/BuiltinFunctions/ByteString.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ From CoqUplc Require Import Prelude.Bytes.
88
From CoqUplc Require Import Prelude.FunctionalNotations.
99
From CoqUplc Require Import Prelude.Option.
1010

11-
From CoqUplc Require Import PlutusV3.CekValue.
12-
From CoqUplc Require Import PlutusV3.Uplc.
11+
From CoqUplc Require Import Uplc.CekValue.
12+
From CoqUplc Require Import Uplc.Term.
1313

1414
Local Open Scope string_scope.
1515
Local Open Scope functional_scope.

theories/PlutusV3/BuiltinFunctions/Data.v renamed to theories/Uplc/BuiltinFunctions/Data.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ From Coq Require Import Lists.List.
44
From CoqUplc Require Import Prelude.FunctionalNotations.
55

66
From CoqUplc Require Import Cbor.Encoding.
7-
From CoqUplc Require Import PlutusV3.CekValue.
8-
From CoqUplc Require Import PlutusV3.Uplc.
7+
From CoqUplc Require Import Uplc.CekValue.
8+
From CoqUplc Require Import Uplc.Term.
99

1010
Local Open Scope functional_scope.
1111

theories/PlutusV3/BuiltinFunctions/Evaluate.v renamed to theories/Uplc/BuiltinFunctions/Evaluate.v

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,18 +3,19 @@ From CoqUplc Require Import Prelude.List.
33
From CoqUplc Require Import Prelude.Monad.
44
Import MonadNotations.
55

6-
From CoqUplc Require Import PlutusV3.CekValue.
7-
From CoqUplc Require Import PlutusV3.Uplc.
86
From CoqUplc Require Import Unicode.String.
97

10-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.Bool.
11-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.ByteString.
12-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.Data.
13-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.Integer.
14-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.List.
15-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.Misc.
16-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.Pair.
17-
From CoqUplc Require Import PlutusV3.BuiltinFunctions.String.
8+
From CoqUplc Require Import Uplc.CekValue.
9+
From CoqUplc Require Import Uplc.Term.
10+
11+
From CoqUplc Require Import Uplc.BuiltinFunctions.Bool.
12+
From CoqUplc Require Import Uplc.BuiltinFunctions.ByteString.
13+
From CoqUplc Require Import Uplc.BuiltinFunctions.Data.
14+
From CoqUplc Require Import Uplc.BuiltinFunctions.Integer.
15+
From CoqUplc Require Import Uplc.BuiltinFunctions.List.
16+
From CoqUplc Require Import Uplc.BuiltinFunctions.Misc.
17+
From CoqUplc Require Import Uplc.BuiltinFunctions.Pair.
18+
From CoqUplc Require Import Uplc.BuiltinFunctions.String.
1819

1920
Local Open Scope functional_scope.
2021

theories/PlutusV3/BuiltinFunctions/Integer.v renamed to theories/Uplc/BuiltinFunctions/Integer.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ From Coq Require Import ZArith.
44

55
From CoqUplc Require Import Prelude.FunctionalNotations.
66

7-
From CoqUplc Require Import PlutusV3.CekValue.
8-
From CoqUplc Require Import PlutusV3.Uplc.
7+
From CoqUplc Require Import Uplc.CekValue.
8+
From CoqUplc Require Import Uplc.Term.
99

1010
Local Open Scope Z_scope.
1111
Local Open Scope functional_scope.

theories/PlutusV3/BuiltinFunctions/List.v renamed to theories/Uplc/BuiltinFunctions/List.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ From Coq Require Import Lists.List.
33

44
From CoqUplc Require Import Prelude.FunctionalNotations.
55

6-
From CoqUplc Require Import PlutusV3.CekValue.
7-
From CoqUplc Require Import PlutusV3.Uplc.
6+
From CoqUplc Require Import Uplc.CekValue.
7+
From CoqUplc Require Import Uplc.Term.
88

99
Local Open Scope functional_scope.
1010

theories/PlutusV3/BuiltinFunctions/Misc.v renamed to theories/Uplc/BuiltinFunctions/Misc.v

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,11 @@ From CoqUplc Require Import Prelude.List.
55
From CoqUplc Require Import Prelude.Monad.
66
Import MonadNotations.
77

8-
From CoqUplc Require Import PlutusV3.CekValue.
9-
From CoqUplc Require Import PlutusV3.Uplc.
108
From CoqUplc Require Import Unicode.String.
119

10+
From CoqUplc Require Import Uplc.CekValue.
11+
From CoqUplc Require Import Uplc.Term.
12+
1213
Definition chooseUnit (Vs : list cekValue) : option cekValue :=
1314
match Vs with
1415
| [VCon Unit; val] => Some val

0 commit comments

Comments
 (0)