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/funind/recdef.ml | |
| 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/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9f52258edf..8014abf651 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] ] ) ) |