diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 797dfbe23..757451882 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r = let add_hints_iff ~atts l2r lc n bl = let open Vernacinterp in - Hints.add_hints (Locality.make_module_locality atts.locality) bl + Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 643f7e99f..07047d016 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -219,7 +219,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF fun ~atts ~st -> begin let open Vernacinterp in let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality atts.locality) + Hints.add_hints ~local:(Locality.make_section_locality atts.locality) (match dbnames with None -> ["core"] | Some l -> l) entry; st end |