2 files changed, 33 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 177c44bcb..c979b8b04 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5003,11 +5003,19 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
     Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
   in
   let cst = Impargs.with_implicit_protection cst () in
-  (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
-  let lem, ctx = Global.constr_of_global_in_context (Global.env ()) (ConstRef cst) in
-  let inst = Univ.AUContext.instance ctx in
-  let lem = CVars.subst_instance_constr inst lem in
-  let lem = EConstr.of_constr lem in
+  let lem =
+    if const.Entries.const_entry_polymorphic then
+      let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in
+      (** Hack: the kernel may generate definitions whose universe variables are
+          not the same as requested in the entry because of constraints delayed
+          in the body, even in polymorphic mode. We mimick what it does for now
+          in hope it is fixed at some point. *)
+      let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
+      let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
+      let u = Univ.UContext.instance uctx in
+      mkConstU (cst, EInstance.make u)
+    else mkConst cst
+  in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
   let eff = private_con_of_con (Global.safe_env ()) cst in
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
new file mode 100644
index 000000000..b736b734f
--- /dev/null
+++ b/test-suite/success/abstract_poly.v
@@ -0,0 +1,20 @@
+Set Universe Polymorphism.
+
+Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x.
+Inductive unit@{i} : Type@{i} := tt.
+
+Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n.
+Proof.
+intros m n P e p.
+abstract (rewrite e in p; exact p).
+Defined.
+
+Check foo_subproof@{Set Set}.
+
+Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n.
+Proof.
+intros m n P e p.
+abstract (rewrite e in p; exact p).
+Defined.
+
+Check bar_subproof@{Set Set Set}.