Commit ad6bc95a authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Fix sections and add Circulation.v to _CoqProject

parent 71ea5d00
Pipeline #12078 failed with stage
in 5 minutes and 6 seconds
......@@ -2,6 +2,7 @@
src/Automation.v
src/Blockchain.v
src/BoundedN.v
src/Circulation.v
src/Congress.v
src/Containers.v
src/Extras.v
......
......@@ -354,11 +354,7 @@ Definition get_contract_interface
transfer := ifc_transfer;
call := ifc_call; |}.
End Blockchain.
Section Semantics.
Context {BaseTypes : ChainBaseTypes}.
Instance chain_settable : Settable _ :=
settable! build_chain
< block_header;
......@@ -673,9 +669,6 @@ Qed.
End ChainTraceTheories.
End Semantics.
Section Blockchain.
Context {BaseTypes : ChainBaseTypes}.
Class ChainBuilderType :=
build_builder {
builder_type : Type;
......
......@@ -6,6 +6,7 @@ From SmartContracts Require Import Containers.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
From SmartContracts Require Import Circulation.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
From Coq Require Import Psatz.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment