Do not try to be clever for term-as-hint interpretation.

The prepare_hint function was trying to requantify over all undefined evars,
but actually this should not happen when defining generic terms as hints through
some Hint vernacular command.

3 files changed, 17 insertions, 14 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2bff610b00..68229dbe26 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1349,13 +1349,7 @@ let add_hints ~locality dbnames h =
 
 let hint_globref gr = IsGlobRef gr
 
-let hint_constr env sigma ~poly c =
-  let c, diff = prepare_hint true env sigma c in
-  let diff, uctx =
-    if poly then Some diff, Univ.ContextSet.empty
-    else None, diff
-  in
-  IsConstr (c, diff), uctx
+let hint_constr (c, diff) = IsConstr (c, diff)
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index eb0f937302..3d4d9c7970 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -199,9 +199,8 @@ val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_
 
 val hint_globref : GlobRef.t -> hint_term
 
-val hint_constr :
-  env -> evar_map -> poly:bool -> evar_map * constr -> hint_term * Univ.ContextSet.t
-  [@ocaml.deprecated "Declare a hint constant instead"]
+val hint_constr : constr * Univ.ContextSet.t option -> hint_term
+[@ocaml.deprecated "Declare a hint constant instead"]
 
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 6cc1940b40..0d32f28d79 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -101,10 +101,20 @@ let interp_hints ~poly h =
       let () = warn_deprecated_hint_constr () in
       let env = Global.env () in
       let sigma = Evd.from_env env in
-      let evd, c = Constrintern.interp_open_constr env sigma c in
-      let h, diff = Hints.hint_constr env sigma ~poly (evd, c) in
-      let () = DeclareUctx.declare_universe_context ~poly:false diff [@ocaml.warning "-3"] in
-      (PathAny, h)
+      let sigma, c = Constrintern.interp_open_constr env sigma c in
+      let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
+      let sigma, _ = Evd.nf_univ_variables sigma in
+      let c = Evarutil.nf_evar sigma c in
+      let c = Termops.drop_extra_implicit_args sigma c in
+      let () = Pretyping.check_evars env sigma c in
+      let diff = Evd.universe_context_set sigma in
+      let c =
+        if poly then (c, Some diff)
+        else
+          let () = DeclareUctx.declare_universe_context ~poly:false diff in
+          (c, None)
+      in
+      (PathAny, Hints.hint_constr c) [@ocaml.warning "-3"]
   in
   let fp = Constrintern.intern_constr_pattern env sigma in
   let fres (info, b, r) =