diff --git a/lib/Parmov.v b/lib/Parmov.v
index 9a07a725f5bd741568d98bc9b23b4934fef13eb0..fa31b673e69da3c6659fb03d8215203a3d0bf19b 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 =>