Merge PR #8974: Fix mod_subst wrt universe polymorphism

1 files changed, 6 insertions, 4 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a3ab250784..248d5d0a0e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,10 +279,12 @@ let rec subst_pattern subst pat =
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
-    if ref' == ref then pat else
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      pattern_of_constr env evd t
+    if ref' == ref then pat else (match t with
+        | None -> PRef ref'
+        | Some t ->
+          let env = Global.env () in
+          let evd = Evd.from_env env in
+          pattern_of_constr env evd t.Univ.univ_abstracted_value)
   | PVar _
   | PEvar _
   | PRel _ -> pat