diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /tactics/class_tactics.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'tactics/class_tactics.mli')
-rw-r--r-- | tactics/class_tactics.mli | 31 |
1 files changed, 28 insertions, 3 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index f1bcfa7d..76760db0 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements typeclasses eauto *) + open Names open Constr open Tacmach @@ -18,10 +20,13 @@ val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit val get_typeclasses_depth : unit -> int option -val progress_evars : unit Proofview.tactic -> unit Proofview.tactic +type search_strategy = Dfs | Bfs + +val set_typeclasses_strategy : search_strategy -> unit -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Hints.hint_db_name list -> tactic +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy -> + depth:(Int.t option) -> + Hints.hint_db_name list -> unit Proofview.tactic val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic @@ -30,3 +35,23 @@ val not_evar : constr -> unit Proofview.tactic val is_ground : constr -> tactic val autoapply : constr -> Hints.hint_db_name -> tactic + +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 *) + ?strategy:search_strategy -> + (** Is a traversing-strategy specified? *) + depth:Int.t option -> + (** Bounded or unbounded search *) + dep:bool -> + (** Should the tactic be made backtracking on the initial goals, + whatever their internal dependencies are. *) + Hints.hint_db list -> + (** The list of hint databases to use *) + unit Proofview.tactic +end |