diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 795582f27..45f92a97f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,7 +10,6 @@ open Pp open Errors open Util open Names -open Nameops open Namegen open Term open Vars @@ -1420,9 +1419,6 @@ let possible_resolve dbg mod_delta db_list local_db cl = (my_find_search mod_delta db_list local_db head cl) with Not_found -> [] -let dbg_case dbg id = - new_tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id)) - let extend_local_db gl decl db = Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db |