diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 00:15:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-27 15:18:11 +0200 |
| commit | b34acd7904dac581b57f7282192a40f1afb870dc (patch) | |
| tree | bf55c06c3571047063abb652b9badd6e1a463cf3 /plugins/ltac/extratactics.ml4 | |
| parent | 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 (diff) | |
[tactics] Turn boolean locality hint parameter into a named one.
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 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 |