Commit 05c93849 authored by Sergey Bozhko's avatar Sergey Bozhko Committed by Björn Brandenburg

Change name of a matched variable

parent 9e805d0b
Pipeline #19181 passed with stages
in 8 minutes and 31 seconds
......@@ -22,7 +22,7 @@ Section State.
Definition service_in (s : processor_state) : nat :=
match s with
| Idle => 0
| Progress j' s => if j' == j then s else 0
| Progress j' speed => if j' == j then speed else 0
end.
End Service.
......@@ -35,4 +35,5 @@ Section State.
Proof.
by move=> j []//= j' s->.
Defined.
End State.
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