diff options
| author | coqbot-app[bot] | 2020-09-23 14:14:58 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-23 14:14:58 +0000 |
| commit | d7b2da080bbfbbc85b3ce19bcda99e06ee355fef (patch) | |
| tree | f8dde56b222424819efe9f9db515ec07c4c9b8b0 /vernac/classes.ml | |
| parent | d9d89ad43e62cfd1dfd3beed924f82d3de7bcc23 (diff) | |
| parent | 69c92f7e83d5d6faf2d0ba830f132114b4746a40 (diff) | |
Merge PR #12977: Statically ensure that only polymophic hint terms come with a context.
Reviewed-by: mattam82
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 02cb60f1cf..b38a249b73 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -41,11 +41,11 @@ let classes_transparent_state () = let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state -let add_instance_hint inst path ~locality info poly = +let add_instance_hint inst path ~locality info = Flags.silently (fun () -> Hints.add_hints ~locality [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst])) () + [info, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -56,14 +56,13 @@ let is_local_for_hint i = itself *) let add_instance_base inst = - let poly = Global.is_polymorphic inst.is_impl in let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality - inst.is_info poly; + inst.is_info; List.iter (fun (path, pri, c) -> - let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in + let h = Hints.IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in add_instance_hint h path - ~locality pri poly) + ~locality pri) (build_subclasses ~check:(not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) |