From 70d557994583bd081787e28f68d627a0833eb9c0 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 2 Nov 2020 17:08:25 -0800
Subject: Remember universe instances of constants in notations

---
 interp/notation_term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_term.ml')

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index c541a19bfd..2979447cf8 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -21,7 +21,7 @@ open Glob_term
 
 type notation_constr =
   (* Part common to [glob_constr] and [cases_pattern] *)
-  | NRef of GlobRef.t
+  | NRef of GlobRef.t * glob_level list option
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
-- 
cgit v1.2.3