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

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

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3c1c470053..9c93f29e06 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
-- 
cgit v1.2.3