diff options
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 02d99d707..2bbb3ac5a 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -15,15 +15,10 @@ open Names open Nameops open Term open Termops -open Sign -open Reduction open Proof_type -open Declarations open Tacticals open Tacmach -open Evar_refiner open Tactics -open Pattern open Patternops open Clenv open Auto @@ -353,8 +348,6 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; error "eauto: search failed" -open Evd - let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) |