Merge PR #12977: Statically ensure that only polymophic hint terms come with a context.

Reviewed-by: mattam82

2 files changed, 12 insertions, 15 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)
 
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 051560fb63..9eac558908 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -62,7 +62,7 @@ let project_hint ~poly pri l2r r =
       cb
   in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-  (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
+  (info, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
 
 let warn_deprecated_hint_constr =
   CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
@@ -89,10 +89,10 @@ let interp_hints ~poly h =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let c, diff = Hints.prepare_hint true env sigma (evd, c) in
-    if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
+    if poly then (Hints.IsConstr (c, Some diff) [@ocaml.warning "-3"])
     else
       let () = DeclareUctx.declare_universe_context ~poly:false diff in
-      (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
+      (Hints.IsConstr (c, None) [@ocaml.warning "-3"])
   in
   let fref r =
     let gr = Smartlocate.global_with_alias r in
@@ -106,20 +106,20 @@ let interp_hints ~poly h =
     match c with
     | HintsReference c ->
       let gr = Smartlocate.global_with_alias c in
-      (PathHints [gr], poly, IsGlobRef gr)
+      (PathHints [gr], IsGlobRef gr)
     | HintsConstr c ->
       let () = warn_deprecated_hint_constr () in
-      (PathAny, poly, f poly c)
+      (PathAny, f poly c)
   in
   let fp = Constrintern.intern_constr_pattern env sigma in
   let fres (info, b, r) =
-    let path, poly, gr = fi r in
+    let path, gr = fi r in
     let info =
       { info with
         Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern
       }
     in
-    (info, poly, b, path, gr)
+    (info, b, path, gr)
   in
   let open Hints in
   let open Vernacexpr in
@@ -140,7 +140,6 @@ let interp_hints ~poly h =
   | HintsConstructors lqid ->
     let constr_hints_of_ind qid =
       let ind = Smartlocate.global_inductive_with_alias qid in
-      let mib, _ = Global.lookup_inductive ind in
       Dumpglob.dump_reference ?loc:qid.CAst.loc "<>"
         (Libnames.string_of_qualid qid)
         "ind";
@@ -148,7 +147,6 @@ let interp_hints ~poly h =
           let c = (ind, i + 1) in
           let gr = GlobRef.ConstructRef c in
           ( empty_hint_info
-          , Declareops.inductive_is_polymorphic mib
           , true
           , PathHints [gr]
           , IsGlobRef gr ))