diff --git a/theories/utils/switch.v b/theories/utils/switch.v
index 869af584448d30adc0ce0156e44e5c65a14daccb..588031079cf29f6b8d2b6c36b2e578e398f84511 100644
--- a/theories/utils/switch.v
+++ b/theories/utils/switch.v
@@ -15,8 +15,8 @@ Fixpoint switch_lams (y : string) (i : nat) (n : nat) (e : expr) : expr :=
   | O => e
   | S n => λ: (y +:+ pretty i), switch_lams y (S i) n e
   end.
-Definition switch_fail (xs : list Z) : val :=
-  λ: "y", switch_lams "f" 0 (length xs) $
+Definition switch_fail (xs : list Z) : val := λ: "y",
+  switch_lams "f" 0 (length xs) $
     switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) #().
 
 Fixpoint map_string_seq {A}