From 511a3eae36d3b57afbbb37b586ef71adf094f8ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Oct 2020 18:41:39 +0200
Subject: Encapsulate the last use of IsConstr in the Hints API.

---
 vernac/comHints.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'vernac/comHints.ml')

diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 9eac558908..b5e53208ca 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -85,14 +85,12 @@ let interp_hints ~poly h =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let f poly c =
-    let evd, c = Constrintern.interp_open_constr env sigma c in
     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, Some diff) [@ocaml.warning "-3"])
-    else
-      let () = DeclareUctx.declare_universe_context ~poly:false diff in
-      (Hints.IsConstr (c, None) [@ocaml.warning "-3"])
+    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
+    h
   in
   let fref r =
     let gr = Smartlocate.global_with_alias r in
-- 
cgit v1.2.3