Commit 4f17a588 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Fix 8.8 compatibility: Try 2

parent e04bac93
Pipeline #12137 passed with stage
in 5 minutes and 3 seconds
......@@ -671,6 +671,7 @@ Qed.
End Theories.
End Step.
Section Trace.
Definition add_new_block_header
(header : BlockHeader)
(baker : Address)
......@@ -776,6 +777,7 @@ Proof.
induction trace; intros to' eq_to; eauto; rewrite eq_from, eq_to in *; eauto.
Qed.
End Theories.
End Trace.
End Semantics.
Class ChainBuilderType :=
......
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