From 915c8f15965fe8e7ee9d02a663fd890ef80539ad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 23 Apr 2015 14:22:42 +0200
Subject: Using tclZEROMSG instead of tclZERO in several places.

---
 tactics/eauto.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eauto.ml4')

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 27c3569da..d738677e5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -609,7 +609,7 @@ TACTIC EXTEND unify
     match table with
     | None ->
       let msg = str "Hint table " ++ str base ++ str " not found" in
-      Proofview.tclZERO (UserError ("", msg))
+      Tacticals.New.tclZEROMSG msg
     | Some t ->
       let state = Hint_db.transparent_state t in
       unify ~state x y
-- 
cgit v1.2.3