diff options
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fb9439d73..2700b2b7d 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -613,6 +613,6 @@ END VERNAC COMMAND EXTEND HintCut | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ let entry = HintsCutEntry p in - Auto.add_hints (Vernacexpr.use_section_locality ()) + Auto.add_hints (Locality.use_section_locality ()) (match dbnames with None -> ["core"] | Some l -> l) entry ] END |