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. --- vernac/classes.ml | 4 ++-- vernac/obligations.ml | 2 +- vernac/vernacentries.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 61ce5d6c4..6743fe79a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -41,7 +41,7 @@ let _ = Goptions.declare_bool_option { let typeclasses_db = "typeclass_instances" let set_typeclass_transparency c local b = - Hints.add_hints local [typeclasses_db] + Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry ([c], b)) let _ = @@ -56,7 +56,7 @@ let _ = (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env()))) info.hint_pattern } in Flags.silently (fun () -> - Hints.add_hints local [typeclasses_db] + Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst'])) ()); Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 3bf0ca0a8..1b864b366 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -612,7 +612,7 @@ let shrink_body c ty = let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = - Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst) + Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) let it_mkLambda_or_LetIn_or_clean t ctx = let open Context.Rel.Declaration in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e1ce4e194..7ca51db78 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -977,7 +977,7 @@ let vernac_remove_hints ~atts dbs ids = let vernac_hints ~atts lb h = let local = enforce_module_locality atts.locality in - Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h) + Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h) let vernac_syntactic_definition ~atts lid x y = Dumpglob.dump_definition lid false "syndef"; -- cgit v1.2.3