diff --git a/analysis/facts/model/ideal_uni_exceed.v b/analysis/facts/model/ideal_uni_exceed.v
index d8fd41ec4a01e40f40a13cd3a3678a6710d21f32..7acaf3be2cf5929fe0043fd0a2cfd86755ebd74a 100644
--- a/analysis/facts/model/ideal_uni_exceed.v
+++ b/analysis/facts/model/ideal_uni_exceed.v
@@ -90,8 +90,8 @@ Section ExceedanceProcStateProperties1.
       [ExceedanceExecution j] for some [j]. *)
   Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
     match pstate with
-    |ExceedanceExecution _ => true
-    |_ => false
+    | ExceedanceExecution _ => true
+    | _ => false
     end.
 
   (** Next, let us consider any schedule of the [exceedance_proc_state]. *)