diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /tactics/class_tactics.mli | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index f64f708de..00c601d28 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -21,7 +21,7 @@ val get_typeclasses_depth : unit -> int option val progress_evars : unit Proofview.tactic -> unit Proofview.tactic val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Auto.hint_db_name list -> tactic + Hints.hint_db_name list -> tactic val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic @@ -29,4 +29,4 @@ val not_evar : constr -> unit Proofview.tactic val is_ground : constr -> tactic -val autoapply : constr -> Auto.hint_db_name -> tactic +val autoapply : constr -> Hints.hint_db_name -> tactic |