diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 2e5647f87..cd2de99be 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -10,7 +10,6 @@ open Names open Term open Clenv open Pattern -open Evd open Decl_kinds open Hints @@ -26,11 +25,9 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - [ `NF ] Proofview.Goal.t -> clausenv * constr + ([ `NF ], 'r) Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic - val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: @@ -46,24 +43,24 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr - "nocore" amongst the databases. *) val auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> hint_db_name list -> unit Proofview.tactic + int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic (** Auto with more delta. *) val new_auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> hint_db_name list -> unit Proofview.tactic + int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic (** auto with default search depth and with the hint database "core" *) val default_auto : unit Proofview.tactic (** auto with all hint databases except the "v62" compatibility database *) val full_auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> unit Proofview.tactic + int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic (** auto with all hint databases except the "v62" compatibility database and doing delta *) val new_full_auto : ?debug:Tacexpr.debug -> - int -> open_constr list -> unit Proofview.tactic + int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic (** auto with default search depth and with all hint databases except the "v62" compatibility database *) @@ -71,19 +68,19 @@ val default_full_auto : unit Proofview.tactic (** The generic form of auto (second arg [None] means all bases) *) val gen_auto : ?debug:Tacexpr.debug -> - int option -> open_constr list -> hint_db_name list option -> unit Proofview.tactic + int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic (** The hidden version of auto *) val h_auto : ?debug:Tacexpr.debug -> - int option -> open_constr list -> hint_db_name list option -> unit Proofview.tactic + int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic (** Trivial *) val trivial : ?debug:Tacexpr.debug -> - open_constr list -> hint_db_name list -> unit Proofview.tactic + Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic val gen_trivial : ?debug:Tacexpr.debug -> - open_constr list -> hint_db_name list option -> unit Proofview.tactic + Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic val full_trivial : ?debug:Tacexpr.debug -> - open_constr list -> unit Proofview.tactic + Tacexpr.delayed_open_constr list -> unit Proofview.tactic val h_trivial : ?debug:Tacexpr.debug -> - open_constr list -> hint_db_name list option -> unit Proofview.tactic + Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic |