From ab6ebfc1f42d96d50763f2dcd6b8322b12613d3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2020 14:58:45 +0200
Subject: Further code simplification in arbitrary hint interpretation.

We reuse the standard code path for term interpretation instead of trying
to mangle it.
---
 vernac/comHints.ml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 0d32f28d79..f642411fa4 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -101,13 +101,10 @@ let interp_hints ~poly h =
       let () = warn_deprecated_hint_constr () in
       let env = Global.env () in
       let sigma = Evd.from_env env in
-      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, uctx = Constrintern.interp_constr env sigma c in
+      let subst, uctx = UState.normalize_variables uctx in
+      let c = EConstr.Vars.subst_univs_constr subst c in
+      let diff = UState.context_set uctx in
       let c =
         if poly then (c, Some diff)
         else
-- 
cgit v1.2.3