From 470943bdf917caf352b5347c8d33fc39699805b0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Nov 2018 12:55:46 +0100
Subject: Fix mod_subst wrt universe polymorphism

---
 tactics/hints.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 77479f9efa..dc3b90211e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1064,12 +1064,12 @@ let cache_autohint (kn, obj) =
 
 let subst_autohint (subst, obj) =
   let subst_key gr =
-    let (lab'', elab') = subst_global subst gr in
-    let elab' = EConstr.of_constr elab' in
-    let gr' =
-      (try head_constr_bound Evd.empty elab'
-       with Bound -> lab'')
-    in if gr' == gr then gr else gr'
+    let (gr', t) = subst_global subst gr in
+    match t with
+    | None -> gr'
+    | Some t ->
+      (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+       with Bound -> gr')
   in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
-- 
cgit v1.2.3