diff options
| author | Gaëtan Gilbert | 2020-01-29 11:34:43 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-29 11:34:43 +0100 |
| commit | f4163cb662983da2bd87a51b7bd1c6e5166b0d74 (patch) | |
| tree | c35c5b5acaf6bb28a949f31ad9f94e7e50ca3742 /vernac | |
| parent | dd86f54cbe7b328b4514c49b8ce1a1c78819f094 (diff) | |
| parent | 25b85ec88a16de73b942564994b7798d8330f396 (diff) | |
Merge PR #11473: Remove dead code in Globnames.
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index c9b5144299..77bc4e4f8a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,13 +42,10 @@ let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state let add_instance_hint inst path local info poly = - let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) - | IsGlobal gr -> Hints.IsGlobRef gr - in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) () + [info, poly, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -61,9 +58,9 @@ let is_local_for_hint i = let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in let local = is_local_for_hint inst in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path + List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) |