aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.mli')
-rw-r--r--tactics/auto.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c887c1bb4..4cd017e5f 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -185,4 +185,4 @@ type autoArguments =
val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
*)
-val h_superauto : int option -> qualid located list -> bool -> bool -> tactic
+val h_superauto : int option -> reference list -> bool -> bool -> tactic