aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.mli')
-rw-r--r--tactics/class_tactics.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 565415a95..21c5d2172 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -40,6 +40,8 @@ module Search : sig
val eauto_tac :
?st:Names.transparent_state ->
(** The transparent_state used when working with local hypotheses *)
+ ?unique:bool ->
+ (** Should we force a unique solution *)
only_classes:bool ->
(** Should non-class goals be shelved and resolved at the end *)
depth:Int.t option ->