aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eauto.mli')
-rw-r--r--tactics/eauto.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index b708949e0..9c23be6f0 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -36,4 +36,4 @@ val eauto_with_bases :
bool * int ->
Term.constr list -> Auto.hint_db list -> Proof_type.tactic
-val autounfold : hint_db_name list -> Tacticals.goal_location -> tactic
+val autounfold : hint_db_name list -> Tacticals.clause -> tactic