diff options
| author | Hugo Herbelin | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /plugins/firstorder | |
| 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')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 6d4d8792f0..f0afa2ec5e 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -204,7 +204,7 @@ let extend_with_ref_list l seq gl = (add_formula Hyp gr typ seq gl,gl) in List.fold_right f l (seq,gl) -open Auto +open Hints let extend_with_auto_hints l seq gl= let seqref=ref seq in diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 40aa169ab2..6462fe9d3b 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 |