diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 18:51:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 16:55:46 +0200 |
| commit | ae9f6d13b63f30168d2eaa2289108a117ad840f7 (patch) | |
| tree | d937467dd5c1913960d58932df19853c93675acb /tactics/auto.mli | |
| parent | dfac5aa2285de5b89f08ada3c30c0a1594737440 (diff) | |
Unplugging Tacexpr in several interface files.
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 1608a0ea6..f68190498 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -39,45 +39,45 @@ val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argume (** The use of the "core" database can be de-activated by passing "nocore" amongst the databases. *) -val auto : ?debug:Tacexpr.debug -> - int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic +val auto : ?debug:debug -> + int -> Pretyping.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic (** Auto with more delta. *) -val new_auto : ?debug:Tacexpr.debug -> - int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic +val new_auto : ?debug:debug -> + int -> Pretyping.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 -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic +val full_auto : ?debug:debug -> + int -> Pretyping.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 -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic +val new_full_auto : ?debug:debug -> + int -> Pretyping.delayed_open_constr list -> unit Proofview.tactic (** auto with default search depth and with all hint databases except the "v62" compatibility database *) 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 -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val gen_auto : ?debug:debug -> + int option -> Pretyping.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 -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val h_auto : ?debug:debug -> + int option -> Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic (** Trivial *) -val trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic -val gen_trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic -val full_trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> unit Proofview.tactic -val h_trivial : ?debug:Tacexpr.debug -> - Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val trivial : ?debug:debug -> + Pretyping.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic +val gen_trivial : ?debug:debug -> + Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic +val full_trivial : ?debug:debug -> + Pretyping.delayed_open_constr list -> unit Proofview.tactic +val h_trivial : ?debug:debug -> + Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic |