From 3c495d6d5773ed3d1566248cf2c65604470ed341 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Mon, 26 Dec 2016 14:04:58 +0100 Subject: [PATCH] Tweak. --- theories/typing/function.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/typing/function.v b/theories/typing/function.v index c5a5ff50..23a767f8 100644 --- 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. -- GitLab