Fix mod_subst wrt universe polymorphism

1 files changed, 4 insertions, 2 deletions

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