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

Tiny cleanup

parent b7a71100
Pipeline #12093 passed with stage
in 5 minutes and 10 seconds
......@@ -456,7 +456,7 @@ Proof.
destruct (address_eqb_spec addr baker) as [addrs_eq|addrs_neq].
- subst.
now rewrite FMap.find_partial_alter.
- now rewrite FMap.find_partial_alter_ne; auto.
- rewrite FMap.find_partial_alter_ne; auto.
Defined.
Global Instance lcb_chain_builder_type : 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