diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-02 17:56:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-02 17:56:05 +0100 |
| commit | e307d0ae873b8b104b9b7cc3bcd538e5faa8456e (patch) | |
| tree | 613f96fa9caf09146f8dbb83a8dfc4189ce09124 /tactics/eauto.ml4 | |
| parent | 2f521670fbd84a118be56d5397dfeb8bcc404f19 (diff) | |
Fixing bug #3226.
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 256f84ba4..21c5a88c7 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 |