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

---
 interp/notation_ops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7a525f84a5..b41160f758 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw =
   match raw with
   | NRef ref ->
       let ref',t = subst_global subst ref in
-	if ref' == ref then raw else
-	  fst (notation_constr_of_constr bound t)
+      if ref' == ref then raw else (match t with
+          | None -> NRef ref'
+          | Some t ->
+            fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value))
 
   | NVar _ -> raw
 
-- 
cgit v1.2.3