From affd9d4557c6eaee78bfc3067f1a2ce37b7aae6a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jun 2016 09:12:57 -0700
Subject: [PATCH] refactor(library/init/meta/base_tactic): merge fail and
 fail_fmt

---
 library/init/meta/base_tactic.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/library/init/meta/base_tactic.lean b/library/init/meta/base_tactic.lean
index 31d2ef6bb7..3fad7ab029 100644
--- a/library/init/meta/base_tactic.lean
+++ b/library/init/meta/base_tactic.lean
@@ -57,11 +57,8 @@ namespace tactic
 variables {S A : Type}
 open base_tactic_result
 
-meta_definition fail (e : string) : base_tactic S A :=
-λ s, exception A (λ u, to_fmt e) s
-
-meta_definition fail_fmt (e : format) : base_tactic S A :=
-λ s, exception A (λ u, e) s
+meta_definition fail {A B : Type} [has_to_format B] (msg : B) : base_tactic S A :=
+λ s, exception A (λ u, to_fmt msg) s
 
 meta_definition failed : base_tactic S A :=
 fail "failed"