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.

1 files changed, 7 insertions, 9 deletions

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 ))