From 05c93849422ae9c10289911dbc28f41d86e96a11 Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 20 Aug 2019 12:58:55 +0200
Subject: [PATCH] Change name of a matched variable
---
restructuring/behavior/schedule/varspeed.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/restructuring/behavior/schedule/varspeed.v b/restructuring/behavior/schedule/varspeed.v
index 138ae8d91..ed1e9cbd3 100644
--- a/restructuring/behavior/schedule/varspeed.v
+++ b/restructuring/behavior/schedule/varspeed.v
@@ -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.
--
GitLab