From eb51b9ef26201424945526400a6a8c830ead40bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Oct 2018 17:10:55 -0700
Subject: [PATCH] chore(library/init/core): avoid `.` as end-of-command and
 empty equations

---
 library/init/core.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/init/core.lean b/library/init/core.lean
index 119498d723..075f373761 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -1207,8 +1207,8 @@ match dec_eq a b with
 | is_true h := is_false $ λ h', absurd h h'
 | is_false h := is_true h
 
-theorem bool.ff_ne_tt : ff = tt → false
-.
+theorem bool.ff_ne_tt (h : ff = tt) : false :=
+bool.no_confusion h
 
 def is_dec_eq {α : Sort u} (p : α → α → bool) : Prop   := ∀ ⦃x y : α⦄, p x y = tt → x = y
 def is_dec_refl {α : Sort u} (p : α → α → bool) : Prop := ∀ x, p x x = tt