/*! Reads next clock value from the file.
If clock kind read from the file is different from the parameter,
the value is not used. */
-void replay_read_next_clock(unsigned int kind);
+void replay_read_next_clock(ReplayClockKind kind);
/* Asynchronous events queue */