Tweak.

3c495d6d · Jacques-Henri Jourdan · f3cce8a0 · 3c495d6d
Commit 3c495d6d authored 8 years ago by Jacques-Henri Jourdan
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -56,8 +56,8 @@ Section fn.
            pointwise_relation A (dist n') ==> dist n') (fn E).
  Proof.
    intros ?? H1 ?? H2.
-    apply fn_contractive=>u; destruct n'; try done; apply dist_S.
-    by apply (H1 u). by apply (H2 u).
+    apply fn_contractive=>u; (destruct n'; [done|apply dist_S]);
+      [apply (H1 u)|apply (H2 u)].
  Qed.
 End fn.