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

---
 plugins/syntax/number.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml
index 89d757a72a..0e7640f430 100644
--- a/plugins/syntax/number.ml
+++ b/plugins/syntax/number.ml
@@ -387,10 +387,10 @@ let locate_global_inductive allow_params qid =
     | Globnames.TrueGlobal _ -> raise Not_found
     | Globnames.SynDef kn ->
     match Syntax_def.search_syntactic_definition kn with
-    | [], Notation_term.(NApp (NRef (GlobRef.IndRef i), l)) when allow_params ->
+    | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params ->
        i,
        List.map (function
-           | Notation_term.NRef r -> Some r
+           | Notation_term.NRef (r,None) -> Some r
            | Notation_term.NHole _ -> None
            | _ -> raise Not_found) l
     | _ -> raise Not_found in
-- 
cgit v1.2.3