From b34acd7904dac581b57f7282192a40f1afb870dc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 00:15:44 +0200 Subject: [tactics] Turn boolean locality hint parameter into a named one. --- plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/g_auto.ml4 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac') 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 -- cgit v1.2.3