aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tauto.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tauto.ml4')
-rw-r--r--tactics/tauto.ml42
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index fdfc2b783..afd0e7799 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -13,13 +13,11 @@ open Hipattern
open Names
open Globnames
open Pp
-open Proof_type
open Tacticals
open Tacinterp
open Tactics
open Errors
open Util
-open Genarg
let assoc_var s ist =
match List.assoc (Names.id_of_string s) ist.lfun with