aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-07 17:26:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-07 18:40:36 +0200
commit38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch)
treec5449cf9c02c97586bf8a8edaa52d05d876d3e94 /plugins
parent2313bde0116a5916912bebbaca77d291f7b2760a (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')
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/firstorder/sequent.mli2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/recdef.ml2
4 files changed, 4 insertions, 4 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 6d4d8792f..f0afa2ec5 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 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
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 700f67a74..cd3f1a5d4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1454,7 +1454,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
Eauto.eauto_with_bases
(true,5)
[Evd.empty,Lazy.force refl_equal]
- [Auto.Hint_db.empty empty_transparent_state false]
+ [Hints.Hint_db.empty empty_transparent_state false]
)
)
)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9f52258ed..8014abf65 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1312,7 +1312,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
Eauto.eauto_with_bases
(true,5)
[Evd.empty,Lazy.force refl_equal]
- [Auto.Hint_db.empty empty_transparent_state false]
+ [Hints.Hint_db.empty empty_transparent_state false]
]
)
)