From e307d0ae873b8b104b9b7cc3bcd538e5faa8456e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 2 Feb 2014 17:56:05 +0100
Subject: Fixing bug #3226.

---
 tactics/eauto.ml4 | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 256f84ba4c..21c5a88c7a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -554,7 +554,15 @@ END
 TACTIC EXTEND unify
 | ["unify" constr(x) constr(y) ] -> [ Proofview.V82.tactic (unify x y) ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
-    Proofview.V82.tactic (unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y) ]
+    let table = try Some (searchtable_map base) with Not_found -> None in
+    match table with
+    | None ->
+      let msg = str "Hint table " ++ str base ++ str " not found" in
+      Proofview.tclZERO (UserError ("", msg))
+    | Some t ->
+      let state = Hint_db.transparent_state t in
+      Proofview.V82.tactic (unify ~state x y)
+  ]
 END
 
 
-- 
cgit v1.2.3