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 /plugins/firstorder/sequent.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 'plugins/firstorder/sequent.mli')
| -rw-r--r-- | plugins/firstorder/sequent.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 40aa169ab..6462fe9d3 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -56,7 +56,7 @@ val empty_seq : int -> t val extend_with_ref_list : global_reference list -> t -> Proof_type.goal sigma -> t * Proof_type.goal sigma -val extend_with_auto_hints : Auto.hint_db_name list -> +val extend_with_auto_hints : Hints.hint_db_name list -> t -> Proof_type.goal sigma -> t * Proof_type.goal sigma val print_cmap: global_reference list CM.t -> Pp.std_ppcmds |