summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/Parmov.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 9a07a72..fa31b67 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -966,7 +966,7 @@ Definition final_state (st: state) : bool :=
| _ => false
end.
-Function parmove_step (st: state) : state :=
+Definition parmove_step (st: state) : state :=
match st with
| State nil nil _ => st
| State ((s, d) :: tl) nil l =>