diff options
| author | Pierre-Marie Pédrot | 2020-09-03 14:28:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-13 19:43:48 +0200 |
| commit | 674dcda367d9ed43f3b0cc8264a0ef10bc7fd751 (patch) | |
| tree | 9fae7950d3c560032688faf98e0aae6d2ee31c8d /vernac/classes.ml | |
| parent | e1a8da8b83aa3ae96ac05c2bc6606aa0719aa64f (diff) | |
Statically ensure that only polymophic hint terms come with a context.
It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
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) |