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/eauto.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/eauto.mli')
| -rw-r--r-- | tactics/eauto.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e2da23aaa..488bc037c 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -10,6 +10,7 @@ open Term open Proof_type open Auto open Evd +open Hints val hintbases : hint_db_name list option Pcoq.Gram.entry @@ -33,6 +34,6 @@ val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list -> val eauto_with_bases : ?debug:Tacexpr.debug -> bool * int -> - open_constr list -> Auto.hint_db list -> Proof_type.tactic + open_constr list -> hint_db list -> Proof_type.tactic val autounfold : hint_db_name list -> Locus.clause -> tactic |